Changes to Metis
- Moved development of Metis to
- Added a
command line argument.
- Fixed a soundness bug in the CNF normalization discovered by Jonathan Prieto-Cubides.
- Fixed two incompleteness bugs in the proof engine discovered by Michael Farber.
Version 2.3: 11 September 2010
- Released sources under the
- Interpret TPTP functions and relations in a finite model to guide
- Process TPTP include directives.
- Handle TPTP block comments.
Version 2.2: 18 March 2009
- Accept input problems in TPTP syntax that contain a mix of CNF and
- Ported to
- Estimate error locations when parsing TPTP problem files.
- Output normalization steps in TSTP format.
Version 2.1: 1 February 2008
- Basic splitting of FOF conjecture formulas.
- Weight clauses using finite models generated from the problem
- Output proofs in TSTP format.
Version 2.0: 21 May 2007
- Complete rewrite, dropping from 13,000 to 10,000 lines of code and
using the new Standard ML basis library.
- The only implemented calculus is ordered resolution and ordered
paramodulation, with no sticky ordering constraints.
- Reads in problems in the new TPTP format.
Version 1.5: 14 January 2004
- Scheduling provers is no longer based on time used, but rather
number of inferences.
- Reads problems in TPTP First-Order Formula (FOF) syntax.
- Simplification of resolution clauses using disequation literals.
- Implemented finite models to guide clause selection in resolution.
- The model elimination prover optimizes the order of rules and
literals within rules.
Version 1.4: 2 October 2003
- Added an ordered resolution prover to the default set.
- Improved resolution performance with a special-purpose datatype
for inter-reducing equations.
Version 1.3: 18 June 2003
- Better benchmarking using new MLton source-level profiling.
- Resolution is more robust and efficient, and includes an option
for clauses to inherit ordering constraints.
- Standardized command-line option processing.
Version 1.2: 19 November 2002
- Standalone version created using the
- Ground-up rewrite of resolution, which now performs ordered
resolution and ordered paramodulation.
Version 1.1: 21 September 2002
- Improved model elimination performance with better caching.
- First-order substitutions are now fully Boultonized.
- The logical kernel performs peep-hole optimizations to keep proofs
as small as possible.
Version 1.0: 18 July 2002
- Released sources under version 2 of the GPL License.