changelog download home install notes performance

What is Metis?

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

Features of Metis

Project Status

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


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

Metis (the moon of Jupiter)