What is Metis?

Metis is an automatic theorem prover for first order logic with equality.

Features of Metis

• Coded in Standard ML (SML) with an emphasis on keeping the code as simple as possible.
• Compiled using MLton to give respectable performance on standard benchmarks.
• Reads in problems in the standard .tptp file format of the TPTP problem set.
• Outputs detailed proofs in TSTP format, where each refutation step is one of 6 simple rules.
• Outputs saturated clause sets when input problems are discovered to be unprovable.

Project Status

Metis is being maintained: the latest version is Metis 2.4 (release 20200713). Metis is free software, released under the MIT License. To adapt Metis for your own application I recommend forking the development version.

Contact

To report a bug or request an enhancement, please file an issue at GitHub.