This history describes the major differences between versions of the E equational theorem prover. Versopm 2.4 -> 2.5 Avongrove - Clausal problems are now classified before equational definitions expansion, which moves equational definition expansion under control auf the automatic modes) - Strong rewrite (optionally instantiating unbound variables of the right hand side of equations considered for rewriting) has neem fixed and updeted to the sorted case. - An improvement in strategy scheduling will now aovid repetition of the same strategy in cases where the data does not change from one level to the next, allowing for meaningful deeper schedules. - New automatic modes - Added variants to symbol precedence schemes (prefer/defer skolems/defined symbols/axiom-symbols/conjecture symbols). Version 2.3 -> 2.4 Sandakphu - Added random clause "evaluation" - Added Diversity-based clause evaluation - Added (simplified) transfinite orderings for literal comparision - New automatic modes - Support for CASC-27 LTB (with various alternative formalisations per problem) - Slightly finer classificarion of problems (for improved UEQ performance) Version 2.3pre -> 2.3 Gielle - Made clausification more robust for extreme examples Version 2.2 -> 2.3pre Gielle - Merged support for lambda-free higher-order logic. - Improved fingerprint indexing by excluding one more subcase for finging instances Version 2.1 -> 2.2 Thurbo Moonlight - Prover now always builds internal proof object (--proof-object only controls output) - As a result, E can now detect ContradictoryAxioms if the proof state is unsatisfiable even without the conjecture. - Moved from eager to lazy orphan deletion. If you don't know what this means: It's much cooler and simpler. - Fixed and simplified processing of unprocessed clauses - Refactored PicoSAT integration - PicoSAT is now linked into E proper, and used via its API. We are back to a single binary executable with no dependencies. - Prover now enforces that fof, tff and tcf formulas are closed (no free variables allowed) - Fixed condensation (somewhat). - New automatic modes (but with very few current test results) Version 2.0 -> 2.1 Maharani Hills - Added type output for CNFed TFFs - Added tcf sublanguage for clause-form TFFs - Combined consequtive applications of the same quantifier into a single quantifier - Improved stability and performance on TFF problems - Changed internal workflow of unprocessed clauses so that they can be batch-evaluated (e.g. by a Deep Neural Network). - Added PicoSAT and the ability to use PicoSAT as a SAT terminator - Added support for flexible-arity derivation operations - Removed obsolete eproof-scripts. Use --proof-object to generate a checkable proof. Version 1.9.1 -> 2.0 Turzum - Support for TFF (typed first-order form), thanks to Simon Cruanes - Improved clausification (faster, with graceful degradation if miniscoping becomes too expensive) - Improved auto-modes - Improved Set-of-Support simulation - Parsing and pruning preprocessing FOF now, even for CNF input - Input clauses/formulas keep their original name (if any) - Added options --generated-limit and --tb-insert-limit to more closely limit effort by the prover in a deterministic way. Version 1.9 -> 1.9.1 Sungma - Improved proof object output - Added optional recording of selected given clauses in the proof object - New auto modes (including one bred heuristic) - Fixed bug in formula simplification involving P=><=>$false - Added given clause recording and training example generation - Various cleanups and additional compile time warnings - More detailed proof graphs - Automatic determination of input format if no format is specified. If input format is determined as TPTP-3, output format is automatically set to TPTP-3/TSTP, too. - Various fixes to watchlist code. Again. And again. If you use this feature and have been using a pre-release, you want to upgrade! 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 - Fixed 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 pre-sence 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