Flooded fens

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

Users

Publications