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 actively developed: the latest version is Metis 2.3 (release 20110926). Users are encouraged to try out or adapt Metis for their own applications. Metis is free software, released under the MIT License.

Contact

To report bugs, request features, or obtain help using Metis, please email metis-users@gilith.com