This history list describes the major differences between versions of the E equational theorem prover. Version 1.9pre016 -> 1.9 Sourenee - Fixed Auto-SInE to never SInE if there is no seed to SInE on - Added output of proof graphs in GraphViz/dot format (coloured, too!) - Added derivation output for CNFization - Fiexed minor bug in proof output Version 1.8 -> 1.9pre016 - Fixed bug that caused proof output to fail in rare cases when the proof was found in preprocessing. - Took out "theory(equality)" from TSTP-output, since FOL-EQ is now assumed the default logic. - Improved proof objects (taking out empty "quote" steps). - Added plenty of new literal selection functions. - Updated auto-modes Version 1.7 -> 1.8 Gopaldhara - Added support for internal proof objects (and option --proof-object) - Added experimental support for strategy scheduling (--auto-schedule) - Minor cleanup and improved auto-mode(s) Version 1.6 -> 1.7 Jun Chiabari - Added prototypical condensing - Significantly improved auto-mode (note that AutoDev mode is, at the moment, intentionally inferior to normal auto mode - use only if you want to compare the effect of inferior ordering implementations!) - Fixed non-critical (but annoying) bug in SOS strategies - Updated eground to support FOF input (if it clausifies to EPR) and to handle unexpected behaviour from MiniSAT - Added interactive batch mode to e_ltb_runner (load large spec once, then keep asking for the status of different theorems via stdin/stdout) - Added enormalize for normalization of terms, clauses and formulas with an oriented rule set without regard for orderings. - Various minor updates and bugfixes Version 1.5 -> 1.6 Tiger Hill - Incorporated minor improvements to the scripts suggested by Jasmin Blanchette - Added support for "Shell" PCL (a more compact form that only records the dependency graph, but not the actual clauses for intermediate results) - Added SInE-axiom filtering and automatic mode for SInE. - Much better heuristics and new auto mode(s) - Even better AutoDev-Mode (use at your own risk ;-) - More convenient command line interface: "eprover --auto" will be good for most people. - Updated manual Version 1.4 -> 1.5 Pussimbing - Fixed bug stopping miniscoping from ever being used - Implemented non-perfect discrimination tree indexing (mostly for comparison with FP indexing) - Fixed indexed paramodulation (no more inefficient top-level overlaps of non-equational literals) - Added further instrumentation for profiling - Implemented (prototypically) folded feature vector indexing and made it the default - Fixed Makefiles to cleanly work with more modern gcc versions - Some more executables are now installed as part of the standard installation. - New auto mode Version 1.3 -> 1.4 Namring - Adapted e_ltb_runner for CASC-23 - Various minor fixes, in particular to proof and answer output - New literal selection function - New auto-modec Version 1.2 -> 1.3 Ringtong - Fixed redundant output resulting in broken proof extraction. - Fixed sub-optimal CNFing (slow, not incorrect) - Implemented e_axfilter as a stand-alone program for pre-processing large problems, and adapted/extended the corresponging libraries. - Added clause evaluation functions that allow the manipulation of the weight based on the presence and frequency of invidual function symbols. - Added answer instantiation output. Version 1.1 -> 1.2 Badamtam - Made stack limit increase fail gracefully (run with default) - Fixed (most) problems with C stream output and signals. The core prover should be clean now. - Cleaned up variable handling and got rid of the ugly second term bank for the given clause - Implemented Bernd Loechner's linear time version of KBO (JAR 36(4):289-310, 2006). - Fixed a serious bug with mixed CNF/FOF input (now it works, previously it did not). - Implemented fingerprint indexing for paramodulation/superposition and backwards rewriting. - Implemented e_ltb_runner for CASC-J5. Probably not generally useful, but comes with extended SinE-like functionality that will be used in the main prover eventually. Version 1.0 -> 1.1 Balasun - Added --help output to eproof - Improved eproof script signal handling. - Fixed automatic memory determination bug on large-memory Macs. - Fixed a number of warnings with the latest gcc version. - Updated proof objects to latest SZS ontology. - Removed some C99-style comments that bothered ancient compilers - Improves TPTP-3/TSTP output (fof sometimes used prefix equal, not infix =). - Fixed bug in the output of symbols with an embedded %. - Added man pages for the major binaries - Added various goal-directed heuristics - Improved pre-processing (cut-off-limit for eq-def-expansion) - Better auto-mode - Optional pre-saturation simplificaton Version 0.999-004->1.0 Temi - Removed old style formulas and CNF algorithm. - Fixed a number of bugs in backwards rewriting. - Made parser more compliant to TPTP 3.5.0 (stricter checking of formula roles) - New GNU-like build and installation system - Fixed one completeness bug in CNF, fixed two serious performance bugs for very large formula CNFization. - Removed dependency on bash (only POSIX Bourne Shell required, I hope) Version 0.999 -> 0.999-004 - Fixed string overflow bug sometimes corrupting auto mode classification (Thanks to Josef Urban for finding it) - Fixed illegal memory access in term formula building (Thanks to Josef Urban for pointing it out). - Updated TPTP-3 parser. - Cleanup of eproof script (thanks to Larry Paulson for bugging me over and over again). Version 0.99 -> 0.999 Longview - Finally got to eliminate the ugly duplicate term cells for terms with rewrite restrictions. This lead to a rather simpler term bank structure, too. - Added better syntactic support for integers and floats. - Removed old '--interprete-numbers' option and associated dead code. - Fixed (hopefully) the learning module, which had suffered from bit rot. It works now, although it ignores FOF axioms for similarity measures. This does not affect the default heuristics. - Made some minor changes to SZS output to make Geoff happy. - Fixed some bugs in the eproof script to make Larry happy. Version 0.91 -> 0.99 Singtom - Introduced new and (maybe) better clause evaluation data type. - Updated install scripts to handle OSes with UCB tail. - Found (and fixed) mismatch between split handling and split documentation (argh!). - New splitting via (reusable) definitions introduced and tested. - Spell-checked manual and (prover) help output. - Better Auto-Mode - Some cleanup. Version 0.9 -> 0.91 Kanyam - Alternative CNF translator with configurable renaming finally done (still needs more testing) (use option --definitional-cnf) - More goal-directed heuristics, and better evaluation of same - Fixed classification bug in auto mode - Result: Better auto-mode - Added option --order-weights for user-defined KBO - Fixed and updated a number of tools, all of which should now work with full FOF format - Fixed TSTP parser to conform to new parenthesizing/precedence handling. Version 0.82 -> 0.9 Soom - Small improvement in unification - Reworked parser - Rebuild indexing data structures with IntMaps (should be much more memory efficient for large signatures) - Added preliminary support for distinct objects and numbers (only ground case so far) - Added support for stronger rewriting (instantiating unbound variables in potential right hand sides) - Implemented TPTP style includes for TPTP/TSTP syntax - Made groundness a stored invariant in term banks (enables more efficient inserting of gorund terms, also helps with literal selection). - Reworked the watchlist (needs more work). - Reworked subsumption by ordering clauses (still need to look at the effect this has on search). - Got rid of ancient options restricting paramodulation (dating back to METOP, and never used) - Modified/rewrote some literal selection functions, taking the AHP (Avoid Head Predicates) property into account (solves some of the interference of the new literal order with heuristic search) - Added simultaneous paramodulation (very useful) - Added goal-directed heuristics. - New auto-mode taking some of the new features into account. - Cleaned up output (--tptp3-out will now also work for output levels <=2 and for final clause sets). - Removed old Auto071 mode (it did not work well with the new internals anyways) and added AutoCASC mode (corresponding to E 0.9pre003 as used in CASC-20). Version 0.81 -> 0.82 Lung Ching - Fixed a bug in find_spec_literal() pointed out by Flavio Ribeira. Might improve performance for large problems with a lot of subsumption. - Added LPO4 variant from Bernd Loechners paper. Much faster - Cleanup of feature stuff (needs more cleaning) - Added support for full first-order logic and clausification - Optimized automatic mode and fixed some ancient automatic mode bugs Version 0.8 -> 0.81 Tumsong - Fixed the SOS propagation bug in splitting. - Overhauled feature vector indexing and added a lot of bells and whistles - Added support for the watch list and watch list based heuristics - Added support for multiple auto modes, including the 0.71 auto mode - (-xAuto071 -tAuto071), the current one, and a developer auto mode (-xAutoDev -tAutoDev, the last two are identical for official release versions, but allow experiments while keeping behavior stable for in-between versions). - Much improved automatic mode (knows more about contextual literal cutting and SOS now) - Improved support for TSTP input and full TSTP output - Added some things to the manual. Yes, really! Version 0.71 -> 0.8 Steinthal - Finally fixed that SOS bug. There still is an SOS problem with splitting (split clauses do not inherit SOS status) that will be fixed for the next release - Added PrioFunDeferSOS - Changed the order of arguments of PCL expression for paramod inferences (seen as a conditional lazy speculative rewrite step now is consistent, i.e. the second one is being applied to an instance of the first one). - Changed the main loop to a more conservative version (_all_ simplified clauses are scheduled for reprocessing) giving a much nicer invariant - Added Defaultweight() and a number of evaluation- and priority functions to improve FIFO (ByDerivationDate, StaggeredWeight(), ...) - Added feature vector indexing for non-unit subsumption - Added contextual simplify-reflect (may change that name - what about contextual equational literal cutting?) - New auto mode, still mostly based on pre-subsumption-indexing test runs - Added epcllemma program that will use various heuristics to suggest lemmata in PCL protocols. 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 compile 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. + Eliminated 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 eliminate _all_ tautologies. Does e.g. remove equality axioms). Thanks to Roberto Nieuwenhuis for the suggestion. Needs testing! + Removed obsolete option "--paramod-with-units-only", eliminated 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