Metis is an automatic theorem prover for first order logic with equality. It implements the ordered paramodulation calculus in Standard ML (SML), with an emphasis on keeping the code as simple as possible. Metis is free software, released under the MIT License, and users are encouraged to try out or adapt Metis for their own applications.
Resources
- Download the latest version of Metis.
- A list of Frequently Asked Questions about Metis.
- Example proofs of CNF and FOF problems in TSTP format.
- Metis has 6 simple kinds of CNF refutation step.
- The archives of the old Metis users mailing list.
Users
- Larry Paulson and Kong Woei Susanto used Metis to reconstruct proofs in an Isabelle tactic called sledgehammer.
- Larry Paulson and Behzad Akbarpour modified Metis to be the core inference engine of MetiTarski.
- Larry Paulson and Markus Wenzel integrated Metis into the Isabelle theorem prover as a tactic called metis.
- Joe Leslie-Hurd used Metis as a platform to carry out a performance comparison of different inheritance schemes for term ordering constraints.
- Joe Leslie-Hurd integrated Metis into the HOL4 theorem prover as a tactic called METIS_TAC.
Publications
- CANONICAL CITATION: Joe Hurd. First-order proof tactics in higher-order logic theorem provers. In Myla Archer, Ben Di Vito, and César Muñoz, editors, Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), number NASA/CP-2003-212448 in NASA Technical Reports, pages 56–68, September 2003. [paper] [bibtex] [talk]
- Joe Hurd. Using inequalities as term ordering constraints. Technical Report 567, University of Cambridge Computer Laboratory, June 2003. [paper] [bibtex]
- Joe Hurd. An LCF-style interface between HOL and first-order logic. In Andrei Voronkov, editor, Proceedings of the 18th International Conference on Automated Deduction (CADE-18), volume 2392 of Lecture Notes in Artificial Intelligence, pages 134–138, Copenhagen, Denmark, July 2002. Springer. [paper] [bibtex] [talk]
Copyright © 2006–2024 Joe Leslie-Hurd