Changes to Metis

Recent Changes

• Fixed a bug that crashed Metis when mutually rewriting disequality literals discovered by Martin Desharnais and Jasmin Blanchett.
• Fixed a bug that prevented clauses from being fully simplified discovered by Martin Desharnais and Jasmin Blanchett.

Version 2.4: 1 March 2018

• Moved development of Metis to GitHub and archiving releases there to enable build reproducibility.
• Added a --time-limit N 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 MIT License.
• Interpret TPTP functions and relations in a finite model to guide clause selection.
• 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 FOF formulas.
• Ported to Poly/ML.
• 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 axioms.
• 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 MLton compiler.
• 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.