This history list describes the major differences between versions of
the E equational theorem prover.

Version 1.6 ->



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-mode

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 defauld 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
