This history list describes the major differences between versions of the E equational theorem prover. Version 0.7 -> 0.71 Puttabong - Added preprocessing of clause sets: Demodulation to get rid of fully defined function symbols, tautology elemination, sorting of clauses - Fixed some bugs, including a bug in subsumption. - Made function symbol ordering more stable by adding more and better secondary criteria (number of occurences in formula...) - Ported to MacOS X, fixed some small portability problems - Fixed bug in compressed PCL output (output of inital clauses came from a different term bank, yielding wrong abbreviations) - Fixed bug in eground (number of clauses in printed DIMACS format was potentially different from stored number of clauses) - Added new and better term ordering schemes and literal selection functions. - Added new weight functions and priority functions to get a better grip on FIFO. - New and better auto-mode (surprise ;-) - Modified the prover to make it run consistently on different architectures. Compile with CONSTANT_MEM_ESTIMATE to get the most from this (see Makefile.vars for documentation). - Added putative TSTP exit status (as a copmpile time option, on by default). Version 0.63 --> 0.7 Dhajea + Changed rewriting implementation from destructive global to cached global. + Changed memory estimator, all limit-based options now use (estimated) bytes as memory units. + New literal selection functions, in particular those avoiding type literals + Rewrote and simplified splitting, added aggressive splitting (splitting of unprocessed clauses) + Added aggressive equality resolution + Added optional unit cutting with unprocessed clauses + New and improved automatic mode + Fixed a bug with --prefer-initial-clauses. Now it works (and often is quite helpful) + Changed output format to native PCL2, optionally with compressed terms. Output level 4 will now print all real inference steps, output level 6 will also print given clause selection, evaluation steps, and subsumption. Implemented epclextract for proof object generation. Note that pattern-based learning now is temporarily broken. After CASC-18 prerelease: + Full virtualization of the core prover - it should now be possible to run several logically independent copies inside one process space (they still share some inference counters and output variables, but nothing that should affect proof search). + Added improved SoS support. You can now specify the SoS by using --sos-uses-input-types and choosing TPTP clause type conjecture or E-LOP query format. Note that there still is a small bug in SoS implementation -- non-SoS clauses simplified with a SoS clause do not enter SoS, but probably should. Since we only simulate SoS anyways, this bug does not lead to a hard incompleteness (but possibly to infinite runs for unsatisfiable problems). It will (hopefully) be fixed for the next release. + Worked on the manual. It is still very incomplete. Version 0.62 --> 0.63 Nuwara Eliya + Added explicit code for the occur-check (shoud be faster than the general TermIsSubTerm()) + Improved interreduction and 1-1-matching (should also help for Subsumption) + Added hooks and code to generate a version with proprietary extensions (under a separate license) + Added SymbolTypeweight heuristic (assigns different weight to non-constant function symbols, constants, predicates, and variables). + Addded support for HPUX again. + Added some new literal selection functions. + Implemented epclanalyse to easily determine certain properties of proofs. + Significantly improved eground, in particular by implementing non-ground splitting (and several pure performance hacks) + New Automatic mode for unit problems (non-Units still use old auto-mode, which probably is sub-optimal with the new calculus refinements) Version 0.61 --> 0.62 Mullootar + Added clause splitting (not yet very good) + Added PNweight clause weight, which assigns different values to symbols and variables in positive and negative literals + Added new features for auto mode (maximum function symnbol arity), very useful for UEQ + New auto mode + Implemented eground (grounds near-propositional proof problems) Version 0.6 --> 0.61 North Tukvar + Added priority function PrioFunPreferNonEqUnits + Addded more literal selection functions + Added option --precedence to allow the user to select partial precedences for the term ordering + Added precedence-generation scheme "const_min", simplified some of the precedence code + Added Waldmeister-like AC handling (on by default), with options --ac-handling and --ac-non-aggressive (read their documentation to see what they do). + Updated proof analysis tools to deal with AC handling, fixed some other annoying things with them (SR was encoded as a generating rule). + Implemented NLweight clause weight, giving different weight to the first occurrence of a variable in a term and later (i.e. non-linear) ones. + Fixed bug in TSM-based weight functions (introduced by pseudo-optimizing me....aaargh!) + Modified frequency-based ordering generation - will now use arity as tie-breaker. + Added new weight generation schemes modarity and modaritymax0 + Fixed some problems with evaluation comparisons on Intel Itanium systems (thanks to Compaqs Test Drive program for access to the hardware!) (in fact, did _not_ yet fix all of them...strange stuff happens!) + Added literal selection functions selecting literals based on orientability. + Rewrote term indexing - can now cope with growing signatures + Added M-literal-selection functions (select positive literals in Non-Horn clauses, not in Horn clauses) + Added --inherit-goal-pm-literals to inherit paramod-literals in goals only + New auto mode once more + Fixed minor bug in RR-literal selection functions Version 0.6 (prerelease) --> 0.6 (Kanchanjangha) + Updated (some) documentation, in particular the help texts of the programs. + Overhauled the manual - it's still very incomplete, but at least not outrightly false anymore (I hope) + Several changes to the CSSCPA code in the EXTERNAL directory (does not affect main prover) Version 0.51 --> 0.6 prerelease + Added various learning heuristics (but documentation is still missing) + Added new literal selection functions taking the ordering into account (and reorganized parts of the proof procedure to allow this). + Added relatively naive LPO cache + Reimplemented LPO for better performance - now faster without the cache + Added support for SOS strategy (with priority function SimulateSOS, does not seem to do very well at the moment) + Enabled soft- and hard cpu time limits simultanously. + Removed legacy option --paramod-strategy (use --literal-selection-strategy instead) + Added option --error-on-empty to allow the catching of certain errors in E-SETHEO + Implemented e2pcl, translating E output to UPCL2 language. + Implemented proof checker for UPCL2. + Eleminated option --no-pdt-indexing (and associated code) + Removed option --discount-vars and associated code (nobody used it anyways, and it lead to code bloat). + Changed option --memory-limit to require an argument. Version 0.5 --> 0.51 (Mim) + Added more literal selection functions playing with range-restriction variations + Moved input format description to scanner object and generalized concept. + Moved signal handling from CONTROL.a to INOUT.a + Included handling for temorary files, abstracted some of the other file stuff + Removed a minor problem from rewriting (affected only proof analysis tools) + Fixed bugs in reproduction and analysis tools + Completed knowledge base management with ekb_create, ekb_ginsert and ekb_delete + Fixed nasty bug in implementation of SimplifyReflect + Added learning heuristics (prototypical) Version 0.5 (prerelease) --> 0.5 (Phuguri) + Fixed a minor bug in clause weight precalculation + Added new literal selection function that does not select literals in range-restricted clauses. Version 0.32 --> 0.5 (prerelease, this is the CASC-16-Version) + Added new weight functions and literal selection functions + Changed an off-by-one error in Saturate...if said to process 0 clauses the prover will now stopp immediately instead of processing one clause. + Added syntax check after clause set has been read - will now complain about additional garbage. + Added option to restrict selection by clause weight and to perform selection only when processing, not when evaluating. + Improved Auto-mode again, based on lots of new test data. + Added another classification to classify_problem (Few, some or many positive ground clauses). Does not seem to help much. + Changed the auto-mode generation tool chain by cutting me and my stupid mistakes out of it. Only che_[HGU]*.c need to be modified now to change the auto mode, and generate_auto.awk will collect all necessary information. Version 0.31a --> 0.32 (Lingia) + Added support to use the prover as a clause set normalizer (basically doing interreduction and subsumption). + Implemented stronger tautology detection (should now eleminate _all_ tautologies. Does e.g. remove equality axioms). Thanks to Roberto Nieuwenhuis for the suggestion. Needs testing! + Removed obsolete option "--paramod-with-units-only", eleminated paramodulation strategies and replaced them with literal selection strategies (once more, thanks to Roberto for pointing out the relationship forcefully enough for me to believe in it ;-). "--paramod-strategy" remains for the moment for backward compatibility, but is mapped to set the corresponding selection strategy. Introduced option "--literal-selection-strategy". + Removed a bug (might have caused incompleteness) from detection of backward-rewritable clauses. + Changed output of result line. Thanks to the literal selection strategy, E will now never terminate with indeterminate result unless the calculus is restricted (and in this case it will say so). + Added more literal selection strategies and option --nogeneration. + Fixed bug in EqnListEqnIs[Strictly]Maximal(). + Removed test for maximality of instantiated negative literals into which the prover paramodulates - it never yielded false anyways in practice. + Added output of the empty clause whenever --print-saturated is selected and the empty clause has been derived. + Added evaluations functions reminiscent of DISCOUNT's MaxWeight. + Added options to control selection (don't yet know if it helps) + Optimized non-unit subsumption and made all stack functions inline - not nice, but that helps a lot. + Made some more stuff inline and optimized matching + Updated automatic mode Version 0.31 --> 0.31a (Jungpana II) + Fixed proofanalyse (prints dependency graph and selects clauses on and near to the proof path as examples) and generate_examples (generates external representations of selected clauses from the -l3 or -l4 protocol + Improved auto-mode once more (only change to the main prover) Version 0.3 --> 0.31 Jungpana + Added TPTP format parser and output routines. + Did some more hacks for evaluation. + Restructured EXAMPLE_PROBLEMS subdirectory (now has the non-obfuscated TPTP and LOP versions of the CASC-15 problems). + Ripped out AVL trees and plugged in Splay trees in clb_ptrees.c. Should save significant amounts of memory, definitly speeds things up. Also reduces code size seriously. I will probably replace some more AVL trees with Splay trees. + Did that: Term Trees and Evaluation Trees now also use Splay trees. The remaning AVL's should be cleaned up sometimes, but are definitly uncritical. + Made $true-term special, it will now no longer carry ext-ref information. Not nice, but saves time and lot's of memory (3 words + Overhead per non-equational literal). + Added options for intermediate filtering of unprocessed clauses, including deletion of (possibly) non-redundant clauses to keep memory consumption in check. The prover no works quite well with whatever memory is offered (but 10 MB is about a rational minimum for non-trivial problems, with 128 MB suggested). + Made all boolean options NoArg options (instead of options with optional argument). + Following a hint by Roberto Nieuwenhuis, implemented real PosUnit-Strategy. I'll have to learn to read sometime... + Added soft cpu limit. + Debugged filtering of unprocessed clauses...first time I ever had to deal with a long overflow (due to my stupidity, no doubt). + Fixed bugs with long option handling and auto-mode (introduced by the changes necessary to support multiple paramod-strategies) + Added filtering for clause copies. + Added removing of clauses in cases of tight memory + Added new weight functions (Sigweight, Proofweight) + Removed entry-index in term banks + Changed rewrite machinery to stop replaced term from being reinserted as super-terms + Brought depanalyze up to working state (it currently prints a dependency graph for clauses, including demodulators). As a side effect, the -l3 option should now work and really print a complete protocol. + Fixed a bug in Equality factoring (it allowed unification between variable and predicate term). + Improved Auto-Mode for heuristic selection, now optimized for standard term ordering (no need for -tAuto anymore). Version 0.24 --> 0.3 "Castleton" + Tested signal handling under HPUX - works fine. + Added a simple auto-mode, changed WFCB interface and added WFCB-Administration for new heuristics-management. + BIG ONE: The command line semantics of the prover changed. Previously, "eprover p1 p2 p3" was equivalent to "eprover p1; eprover p2; eprover p3", but that did not make to much sense and complicated quite some things. Now it is equivalent to "cat p1 p2 p3| eprover". This allows you to modularize your specifications to a certain degree. + Added HCB-Administration and interface, rewrote heuristics-code. Does now need user-level documentation badly! + Wrote some of this documentation ;-) See CLIB/DOC/eprover.tex + Added proof output (machine friendly only, will need tools to post-process). + Hacked a lot of scripts for test runs and evaluation. + Fixed an extremely stupid bug (4 times over) in precedence generation, fixed a lot of bugs in weight generation that were masked by this one. Removed TOGenerateDefaultWeights(), as it was redundant anyways. Moved TOGenerateDefaultPrecedence() to che_to_precgen.[ch], were it belongs. + Fixed incompleteness caused by too strong subsumption. + Added auto-mode for heuristic selection and ordering selection. Version 0.23 --> 0.24 "Yunnan" + Fixed one more bug (subsumption of negative literals without recomputation of maximal literals) + Added simple signal handler to make --cpu-limit work on more platforms (should now work on all versions of Linux and Solaris, untested on other platforms). + Restructured part of the code, moved ProofState object deeper to allow clean coding of an auto-mode. + Variables do not have external references anymore -> saves time and space, and fixes half a bug. + Did some testing. "eprover -x Standard --memory-limit=192 --cpu-limit=300" on a SUN Ultra-10 Workstation should be able to solve about 1312 problems from the TPTP version 2.1.0. Version 0.22 --> 0.23 "StopGap" + Fixed bugs in LiteralCompare() (main reason for new release) + Added paramodulation with maximal variable sides (makes the prover more complete ;-) + Wrote some simple precedence generation schemes for the orderings + Added unit-paramodulation strategy for Horn Clauses form [Der91]. Very strong except for the TPTP PLA domain. Version 0.21 --> 0.22 "Risheehat" + Removed rewrite cruft (see last version change) + Unified term banks for processed and unprocessed clauses, optimized rewriting + Optimized unification + More verbose and more correct statistics + Removed a long-standing (but basically user-invisible) memory allocation bug from cto_ocb.c. Yes this is important (to me...)! + Optimized rewriting (again) with better use of normal form dates. Helps some, but not as much as I would have expected - perhaps a lingering bug? + Removed some more cruft, cleaned up term type + Simplified clause type. + Simplified equation type, replaced boolean properties with bit properties after profiling showed that shared terms are so efficient that clause and equation cells contribute significantly to memory consumption. + Implemented simple non-unit-subsumption. Prover now works in some fashion on non-unit problems (i.e. would not come in as last in CASC-15). + Did some more profiling on KBO and found out that new implementation does help -> it is now the default. + Implemented weight-generation schemes for KBO + Took variables out of the term trees in the term bank. + Implemented pre-hashing for term bank terms. Works great! + Changed default weight for terms and variables -> usually better performance. Currently, use -i1 -i1 for old default behaviour. + Decided to give cool names to releases. + Optimized rewriting once more...marginal improvements. Version 0.2 --> 0.21 + Rewrote rewrite machinery (still some cruft to remove) and simplified proof procedure + Added --version option for GNU's sake + Fixed still more serious (if seldom occuring) bugs + Added --memory-limit option (works only on systems with rational setrlimit()) + Added second implementation of KBO (no improvement *sigh*) + Some cleanup Version 0.1 --> 0.2 + Improved indexing + Stronger unit-subsumption + Fixed lots of serious bugs + Improved KBO efficiency