Changes (21-02-2014): - fixed some bugs regarding the output of partial answers - added a flag "keep_proof_substitutions_flag" Changes (20-11-2013): - changed release string date format to dd-mm-yyyy, because I could never remember whether the old one was meant to be yyyy-mm-dd or yyyy-dd-mm - added learning facilities for closing lemmas - fixed some bugs regarding the level cut in combination with simplifications of split literals that get merged into a single literal Changes (30-07-2013): - fixed a bug in the clause printing involving input variable names Changes (08-02-2013): - streamlining of unification and subsumption - changed handling of delta-clauses (now exist only temporarily) Changes (18-01-2013): - experiment: switched of subterm indexing for atleast-literals Changes (10-01-2013): - added the OWL to TME converter O2DEval by Sonja Polster to the scripts directory Changes (07-01-2013): - many under-the-hood changes in preparation for an implementation of the Given-Clause-Algorithm (still work in progress, an experimental version is available already though, see manual) - upgrade to version number 1.4 Changes (23-12-2012): - fixed an incompatibility between atleast-rules and the level-cut optimization Changes (14-12-2012): - more bugfixes concerning the "atleast_successors_as_dois" flag Changes (10-12-2012): - bugfixes concerning the "atleast_successors_as_dois" flag Changes (31-10-2012): - added the option to use the unique name assumption instead of generating inequations when processing $$atleast-literals (see new flag "atleast_successors_as_dois"). Changes (17-10-2012): - integrated Markus Benders unique-name-assumption handling (distinct object identifiers) Changes (10-10-2012): - added set_max_model_size_for_preds command, see manual Changes (03-08-2012): - added the loganswer webservice proxy interface by Markus Bender to the installation package Changes (25-06-2012): - fixed parser to handle unit clauses without parentheses Changes (14-06-2012): - slight change to the stdout output of ekrhyper_ltb.pl Changes (06-06-2012): - fixed a timer problem in the ekrhyper_ltb.pl script (can now handle "limit.time.problem.wc 0") Changes (29-05-2012): - Fixed an inefficiency problem in the clausifier which could cause an exponential memory blow-up on deeply nested terms. Changes (25-05-2012): - fixed another bug involving disjunctive atleast-literals and redundancy Changes (18-05-2012): - fixed a bug causing a crash when using do_models with atleast-literals Changes (05-04-2012): - fixed bugs in the treatment of atleast-literals caused by the new simplification Changes (28-03-2012): - extended capability of simplification - fixed a soundness bug: premise redundancy is now optional ("premise_redundancy_flag"), if set to true (default) it disables subsumption within news Changes (27-03-2012): - added extensive simplification operations (demodulation, subsumption etc.) on clauses during processing - "simplify_input_flag" allows turning off/on simplification during reading of input (default: on) - setting new flag "proper_subsumption" on on (default) will use real (subset-based) back-subsumption - fixed sorting of positive clause literals: they will stay in the order as entered, unless "sort_heads" is set to on (default) - splitting now makes use of the negative units (if "negative_units" is set to on), by preferring disjunctions with many contradicted literals Changes (31-01-2012): - numbers that exceed the integer limit will now be trated as strings instead of causing a crash Changes (26-01-2012): - fixed a bug in the save_lemmas command Changes (05-01-2012): - 'make clean' now deletes generated parser and lexer - all tab-characters have been replaced by ordinary spaces - attempt to create code convetions / a code style Changes (05-12-2011): - fixed a bug which could cause splitting with atleast-literals to crash Changes (17-08-2011): - fixed a bug in the recent blocking implementation Changes (22-07-2011): - modified the blocking to work like in "Optimized Reasoning in Description Logics using Hypertableaux" (Motik, Shearer & Horrocks) Changes (17-07-2011): - added a DL-style blocking rules to the $$atleast-literals (flag 'dl_blocking', false by default) Changes (06-07-2011): - fixed more bugs in the atleast-literals - added a few (experimental) redundancy checks Changes (04-07-2011): - fixed a problem with the groundedness-recognition of atleast-literals Changes (21-06-2011): - fixed a soundness bug caused by a change in the 20-06-2011 version. Changes (20-06-2011): - further changes to the $$atleast-predicates, see manual - when using the finite model transformation and the verbosity is set to at least 3, the automatically added clauses will be printed to stdout at the start of executing the #(run) command. Changes (13-06-2011): - added the builtin evaluable $$atleast/3-predicate, see manual Changes (18-05-2011): - parser fix to allow nesting of commands Changes (11-04-2011): - bugfix for the do_models-command Changes (17-11-2010): - dropped "webservice_interface_type" parameter, changed $$wsq/3-literal specification instead. Changes (16-11-2010): - added basic webservice functionality, see flag "wait_for_webservices" and parameter "webservice_interface_type" in the manual. Requires an external interface. Changes (07-09-2010): - switched from associated lists to hash tables for certain parts of indexing; shows drastic improvement on very large input, but could result in memory problems, so this is experimental for now Changes (29-06-2010): - reversed recent clausifier changes, they were not paying off and may be unsound Changes (27-06-2010): - general cleanup for CASC, shift to version number 1.1.4 - modifications to clausifier, which now tends to create fewer clauses at the cost of more new symbols Changes (22-06-2010): - changed 'read_and_print_only', so that commands and the TPTP 'include'-directives will still be evaluated. This also means that 'read_and_print_only'-mode can be changed again at runtime by applying the appropriate parameter switch. Changes (10-06-2010): - changed 'read_and_print_only' from flag to parameter; i.e. valid values are no longer true/false, but 0 (default, normal proving), 1 (print input in canonical Prolog and discard it immediately, no proving), and 2 (like 1, but use pretty printing syntax) Changes (10-05-2010): - fixed a bug that could cause looping during the partitioning - fixed several memory leaks and inefficiencies that could cause problems when solving many problems and saving/reloading states frequently Changes (29-07-2009): - further changes to the memory limiting Changes (27-07-2009): - more aggressive garbage collection when memory limit is active Changes (18-07-2009): - final cleanup of the ltb-script Changes (17-07-2009): - extended interrupt handling - new command: set_memory_limit(MB) Changes (15-07-2009): - some minor syntax adjustments for CASC Changes (08-07-2009): - fixed a bug related to is/2 which could cause crashing in #(print_current_compiled_rules) and #(load_previous_input_state) Changes (25-06-2009): - fixed the TPTP-parser to accept the index-command. Changes (03-06-2009): - unreachable query clauses will not be deactivated when partial answers are being computed Changes (25-05-2009): - leading uppercase bug fixed in 'print_safe_fof' Changes (24-05-2009): - added proper version name Changes (18-05-2009): - fixed a bug that would cause a crash in SYN075-1, of all places Changes (14-05-2009): - float bug fixed in 'print_safe_fof' Changes (13-05-2009): - new flag 'print_safe_fof' Changes (12-05-2009): - minor internal details changed - new flag 'ensure_safe_filenames' Changes (01-01-2009): - fixed a problem in the complement splitting, where splits could occur where they should not Changes (17-12-2008): - added a fairly aggressive use of the OCaml garbage collector. This keeps the memory usage in check, but might be too much. Should be considered experimental for now, might be dropped again. Changes (14-12-2008): - fixed a bug in the previous changes - this version will output a temporary log-file 'ekrh_log.txt' in the current directory Changes (13-12-2008): - added a new flag '#(set_flag(sort_clauses_for_answer_computation, ))', with being 'true' or 'false' as usual, default 'false'. At 'true', delta clauses will be used in the first evaluation round, units and lemmas will be inserted as deltas right away, and delta literals within clauses will be sorted to the front. All in all this improves the generation of partial answer units. It has no effect on correctness and completeness. Changes (12-12-2008): - last maximum weight is now displayed correctly when the derivation is interrupted due to a maximum weight limit - fixed a bug where a non-focus-variable would be treated like a focus-variable - fixed a bug which caused the creation of too many partial answers - fixed a bug which caused the maximum weight limit to halt derivations by mistake Changes (11-12-2008): - if an answer variable is in use and the tableau has been closed with a proof which not contains the answer variable, then the command '#(print_answer_units)' will print a single unspecific unit '$answer'. - added an ew parameter '#(set_parameter(max_weight_limit, ))', with being an integer. If n is zero or greater, then E-KRHyper will halt the derivation as soon as the weight limit exceeds the limit given by n. A 'NO RESULT' output will be given. If set to -1 (default setting), then no such limitation will be used. - partial answers are now also given if the query clause does not contain a special answer variable Changes (10-12-2008): - added a new parameter '#(set_parameter(lemmas_at_weight, ))', with being an integer. If n is zero or greater, and the term weight bound is in use, then the command '#(save_lemmas)' will only save those lemmas which were derived before the weight bound exceeded n. If set to -1 (default setting), then '#(save_lemmas)' will save all lemmas. Changes (09-12-2008): - added a new parameter '#(set_parameter(max_proof_depth, ))', with being an integer. If n is zero or greater, then E-KRHyper will halt the derivation as soon as a proof would exceed the depth given by n. A 'NO RESULT' output will be given. If set to -1 (default setting), then no such limitation will be used. - '#(insert_lemmas)' has been sped up considerably. Changes (08-12-2008): - added a command '#(print_last_max_weight_used)', which prints the last maximum weight limit in use Changes (04-12-2008): - the OCaml garbage collection is now invoked more frequently, this should help with the increased memory usage on 64bit architectures Changes (01-12-2008): - the result statistics will now display the correct weight value even when no weight increase occurred (previous versions always showed '-1' instead of the correct initial value, which could be different from '-1') Changes (25-11-2008): - fixed a filename-related bug which appeared in the last version Changes (14-11-2008): - fixed yet another a bug in the partitioning which could cause too many clauses being dropped Changes (14-11-2008): - partitioning change: if no specific variable has been declared for answer computation, then the partitions will be activated for any negative clause Changes (13-11-2008): - fixed a bug in the partitioning which could cause too many clauses being dropped Changes (25-10-2008): - (hopefully) fixed a bug in the '#(save_lemmas)'-command; this should prevent the OCaml-'List.nth'-error which could occur under certain circumstances Changes (23-10-2008): - automated partition assignment: assigning clauses to predicates can now be done automatically, using the command #(compute_partitions). External assignment computation is no longer necessary that way, it will be performed internally instead. A full rundown on partitioning usage: Partitioning is intended for speeding up answer computation. It will only take effect when a TPTP-FOF conjecture is among the current clauses, and a variable within the conjecture has been declared relevant for answer computation, for example with: #(compute_answer_for_tptp_fof_variable('FOCUS')). Remember that this declaration must be made before any clauses (including the conjecture(s)) are entered into the prover. After entering the knowledge-base clauses, use #(compute_partitions). to compute the partitions. Then activate partitioning with #(activate_partitioning). (If partitions are computed, but partitioning is not activated, then the full clause set will be used during the tableau derivation. If on the other hand partitioning is activated without any partitions having been computed, then the derivation will start with an almost empty clause set (containing only the conjecture), since no clauses have been assigned to partitions, which means the partitions are empty.) Starting the derivation with a properly initialized partitioning will then cause E-KRHyper to remove all clauses which are certain to be irrelevant for the refutation of the conjecture. Note that clauses entered into E-KRHyper after '#(compute_partitions)' are exempt from partitioning - they will always take part in the derivation, unless partitions are recomputed with another call to '#(compute_partitions)'. Partition usage can be deactivated with #(deactivate_partitioning). Previously computed partition assignments remain in the system, there is no need to recompute them if partitioning is to be re-activated after deactivating. Changes (02-10-2008): - alternative approach to lemmas: if E-KRHyper has been interrupted during a derivation, then any lemmas can be saved using #(save_lemmas). Lemmas saved this way can be reinserted into the input later on using #(insert_lemmas). Only one set of lemmas is kept in storage. '#(save_lemmas)' will delete previously saved lemmas. The lemma storage can be cleared with #(clear_lemmas). Changes (30-09-2008): - knowledge-base partitioning: there are now a number of commands which control knowledge-base partitioning. When partitioning is in use, such clauses which are certain to be irrelevant for the refutation of a conjecture will be taken out of the derivation process. Using partitioning requires several steps. First of all, clauses must be assigned to predicates. This is done with the command #(assign_clause_to_predicate(, /)). ... which assigns the Clause to a predicate with the name Predicate and the specified arity. The clause will only be used during a derivation if it has been assigned to a predicate occurring in a (TPTP-FOF) conjecture. A clause can be assigned to multiple predicates by using multiple commands. Determining the assignments must be done outside of E-KRHyper at the moment, by hand or by preprocessing scripts. Assignments and partitioning only take effect when partitioning is activated, which is done with #(activate_partitioning). Likewise, it can be turned off again with #(deactivate_partitioning). Changes (12-09-2008): - added a parameter 'print_input_count', which can be set using the command #(set_parameter(print_input_count, n)) with n being an integer (default setting is n=0). If set to a value larger than zero, then E-KRHyper will report the number of processed input clauses while reading a file, and it will do so for every n-th clause. I.e. n=1 means the number will be reported after every clause, n=100 means the number will be reported after every 100th clause etc. This can be useful for debugging large input files. Changes (15-08-2008): - fixed a bug concerning a combination of level cut and the detection of the empty clause hidden among minimizable delayed disjunctions; the latter can cause a branch closing which is not well reflected in the generated proof term so far, since the consecutive minimizing of a term is not particularly integrated into all aspects of the reasoning yet (would have to be displayed as a series of sup-right inferences). This means that the proof term will not necesarily contain all clauses relevant for the minimizing, and rather show a single minimization step. Therefore the level cut function will possibly not properly detect the necessity of a unit for the closing, and perform an illegal cut. The fix prevents a level cut in the case of delayed disjunction closing. A cleaner solution would be an extension to the proof term generation, which will be implemented in the future. Changes (28-07-2008): - fixed a bug in the clausifier's variable renaming Changes (27-07-2008): - final cleanup of the ReadMe-file for CASC Changes (26-07-2008): - modified the TPTP-parser so that equational literals are read properly both with and without surrounding parentheses Changes (18-07-2008): - fixed a problem with the weight-based iterative deepening which caused a hang-up on TPTP-problem ALG135+1 Changes (17-07-2008): - changed the CASC-configuration file so that all input will be read as tptp-syntax - fixed a bug which could cause the creation of domain-enumerating clauses even when there was no need for them (thanks to Geoff Sutcliffe for pointing out a symptom of this) - fixed a bug where overweight negative clauses could be identified as redundant in spite of not being so - fixed a soundness problem caused by inconsistent orientation of certain equations - overweight clauses which can be minimized to the empty clause will now lead to earlier closing Changes (15-07-2008): - updated 'readme_casc_install.txt' Changes (05-07-2008): - minor change in the config.tme-file for the CASC-installation: reduced output Changes (01-07-2008): - fixed an indexing bug where clauses could be subsumed by larger clauses. Changes (30-06-2008): - fixed a soundness problem that had crept into the last version. This bug was only present in the 27-06-2008 version. - there are some new commands regarding knowledge-base partitioning. This is work in progress, the commands will not do anything of actual use yet. Changes (27-06-2008): - added Peter Baumgartner's flag 'pretend_range_restricted_input', which allows turning off the range-restricting even if the clauses would normally require it. - added command 'print_tptp_fof_lemma', which essentially wraps the output provided by 'print_lemmas' into a single conjunctive TPTP first-order formula. - added proper SZS output for TPTP first-order formula input. As E-KRHyper allows mixed input (for example some clauses in Protein-format, some clauses in TPTP-CNF and some formulas in TPTP-FOF), for the purposes of determining the SZS output the input will count as TPTP-FOF as soons as there is at least one TPTP first-order formula. Note that mixed input may make things complicated - for example, enter an unsatisfiable CNF-problem and a countersatisfiable FOF-conjecture, then E-KRHyper will halt with a SZS Theorem result, even though the conjecture had nothing to do with closing the tableau and would actually have resulted in SZS Countersatisfiable if computed on its own. Changes (26-05-2008): - fixed a bug regarding variable equations (X=Y) - fixed a bug with the input layering that could occur if a computation was interrupted and then restarted Changes (08-05-2008): - added command 'print_lemmas', which prints all (non-input) units that have been derived before the first branch split. This is very experimental so far. Changes (29-02-2008): - removed a debug message that had been left in by accident Changes (27-02-2008): - fixed a bug where a non-range-restricted (i.e. non-ground) non-equational input unit would be insufficient to trigger the generation of the domain enumerating clauses, even though these would be required to derive the ground terms used to purify some non-Horn input clause with shared variables in the positive literals Changes (25-02-2008): - fixed a bug in the clausification algorithm for FOF-TPTP input that could cause bad variable renamings in complex formulas Changes (22-02-2008): - fixed a bug regarding redundant clauses: when inferencing had been interrupted by SIGINT, input clauses that had become redundant would not be restored to non-redundant upon a restart of inferencing - work in progress: many incomplete changes that have no effect yet Changes (31-12-2007): - finite model transformation is activated by #(set_flag(finite_model_transformation_flag, true)). The flag must be set to true before clauses are entered. - domain enumerating clauses are no longer created when finite model transformation is in use - the domain size for finite model transformation can be set with #(set_parameter(finite_model_transformation_domain_size, n)). If n=0, then the domain size will be set to equal the number of unique constant symbols in the current input (i.e. before the transformation). If n is a positive integer, then the domain size will be set to that number. The parameter has no effect if the aforementioned flag has not been set. Changes (29-12-2007): - fixed a bug in the finite model transformation Changes (22-12-2007a): - fixed a bug in the symbol hashing in subterm indexing Changes (22-12-2007): - first steps towards finite model computation transformation: set the flag 'prefer_dom_literals' to true in order to select body domain literals first during derivation. Actual transformation of the clause set must be done manually first, for now. Changes (19-12-2007): - fixed a bug involving timers when running piped input - added optional szs output for a timeout ('szs status GaveUp') - the partial answer units ('$partial_answer'/3) now have three arguments instead of two. The third argument is a list of those literals that did not unify with the current facts, in the order used by E-KRHyper. The first element of this list is thus the literal that failed the unification, and the other literals in the list were not tried. Changes (14-12-2007): - computation of partial answers: if an answer is to be computed for a TPTP FOF conjecture, the it is now possible to derive partial answers that can be displayed if the tableau derivation gets interrupted. Partial answers will be computed if the flag 'compute_partial_aswers' is set: #(set_flag(compute_partial_answers, true)). This will only have an effect if the regular aswer computation is also in place. If the derivation process is interrupted by a timeout or a SIGINT, then the partial answers can be displayed with the command #(print_partial_answer_units). See the manual for the syntax of a partial answer unit. Changes (12-12-2007): - added commands to stop timers: '#(stop_wallclock_timer)' and '#(stop_virtual_timer)' Changes (10-12-2007): - fixed some speed issues with the recent changes Changes (05-12-2007): - IMPORTANT: E-KRHyper now requires OCaml 3.10.0 for compilation - smaller bugs/annoyances regarding input over the KRH-prompt have been fixed: change of input type now works, interruptions (STRG-C) are handled more consistently - new command '#(clear_builtin(p/n))': corresponding to '#(clear_builtins)', which clears all builtin symbols to treat them as normal symbols without special functions, there is now the command '#(clear_builtin(p/n))' for the clearing of a specific builtin symbol 'p' with arity 'n'. - addition of timers: the operation of E-KRHyper can now be limited by two types of timers, a wallclock timer and a virtual timer (warning: the latter type is unsupported by Cygwin and requires a 'real' Unix/Linux). A timer can be started with '#(start_wallclock_timer())' or '#(start_virtual_timer())' respectively, where must be a floating point number representing the seconds until the timeout interruption shall occur. The behaviour of E-KRHyper upon a timeout interruption can be modified by setting the parameter 'timeout_termination_method'. If set to 0 (as per default), then E-KRHyper will exit. If set to 1, E-KRHyper will stop executing the current command and proceed to the next one (if the program is reading commands from a file) or wait for the next one (if the program is receiving commands from the KRH-prompt). The setting 3 is possible, but the corresponding method (see manual) has not been completely implemented yet, so this is not recommended. - saving and retracting of input clauses: in addition to the '#(clear_rules)' and '#(abolish(p/n))' commands, there is now a different method for the undoing of input clauses. The command '#(save_input_state)' will cause E-KRHyper to save the current set of input clauses. The command '#(load_previous_input_state)' will then load the most recently saved state of input clauses, and all clauses that were entered after its saving are discarded. It is possible to save multiple input states, and multiple calls to '#(load_previous_input_state)' will then iterate backwards over the saved states. The index is not rebuilt from scratch whenever a state is loaded, so this new feature is fast and useful when doing experiments with a large set of input clauses like an ontology: the ontology is entered as usual, then the state is saved, and then additional problem clauses can be entered, tested in conjunction with the ontology, and then be removed again by loading the saved state, allowing further experiments with different problem clauses. Note that '#(clear_rules)' and '#(abolish(p/n))' override saved states and completely remove clauses from the system; any clause removed by these commands will not reappear by loading an earlier input state. Changes (29-11-2007): - another bug in the abolish-command fixed - added a wallclock timer and a virtual timer - minor parser extension to cover numbers containing 'e' (like 2.243e4) Changes (28-11-2007): - a bug regarding builtin predicates and the abolish-command has been fixed - the clause stratification algorithm has been reverted to a version closer resembling that in the original KRHyper; this fixes a stratification bug, but the handling of equations in stratification remains questionable, making further research necessary New Features (26-11-2007): - reworking of the native tme parser: strict separation of arithmetic and normal terms seems impossible when evaluables and non-evaluables are allowed to share identifiers and shift-reduce-conflicts are to be avoided. The current solution mimics the behaviour of the original canonical tme parser as well as of the parser in SWI-Prolog; syntactically bad input is accepted, and the system relies on the subsequent evaluation to complain. New Features (22-11-2007): - bugfixes regarding 0-ary predicates, the command prompt and infix operators in tme; still work to do on the latter - additional evaluables New Features (21-11-2007): - Some bugs fixed with the abolish/1-command. - Parsers for non-canonical tme and for fof-tptp now also work in the interactive mode ("KRH>"-prompt). Commands ("#()") should be understood in any input mode, but if clauses and formulas are to be entered, then the input mode must be switched accordingly to prevent a parsing error. New features (14-11-2007): Some additions have been made to the treatment of first order formula input in the TPTP-format: - By default, 'conjecture'-formulas are negated before the internal clausification. This can be turned off with #(set_flag(tptp_fof_negate_conjectures, false)). EXPERIMENTAL: - In many problems a conjecture will be clausified into a clause of the form false :- . A refutation for the problem is found when all literals in have unified with positive unit clauses. The bindings of the variables in can be extracted from the subsequent proof output, but this is cumbersome. If the binding of a particular conjecture-variable is of interest, then here is a simpler way to get this information. The declaration #(compute_answer_for_tptp_fof_variable('')). will give the variable with the name a special status, and its binding(s) will be stored separately (non-Horn clauses allow for multiple bindings within a single derivation). After a derivation run that ends in a refutation, the bindings can be listed with the command #(print_answer_units). For each binding term , a unit clause will be printed in the form of '$answer'(). NOTES: - The variable in the declaration must be given in single quotes. - The declaration 'compute_answer_for_tptp_fof_variable' must be made before the input conjecture is read, in a different file (this is due to the way the file parsers work - a limitation that should be fixed soon). For now a suitable place for this declaration is the configuration file, or a separate declaration file that is read before the TPTP-fof input. - The answer computation involves additional clause transformation during the clausification process. A clausified conjecture of the form false :- . will be transformed into '$answer'() :- . false :- '$answer'(X). New features (01-11-2007): - accepts input files in tptp-syntax (fof and cnf) - accepts input files in tme-syntax directly (no need for preprocessing into canonical 'prefix'-form) - domain clauses are generated internally, making the preprocessor unnecessary for this task See manual/help for further details. The new input types are only acceptable for files. Interactive input into E-KRHyper's command prompt must still use the original syntax. Commands ('#(run).' etc.) are accepted in all input types. The domain enumerating clauses are now generated b E-KRHyper itself. Using the preprocessor pre.pl with the -ehyper flag (as recommended in older versions) is unnecessary and will cause a slight delay due to the domain clauses being generated several times. Note that the preprocessors do not accept tptp-syntax at all. Use of the preprocessor is only recommended when backwards compatibility is required, that is, for input files in non-canonical tme form.