What is the opentheory tool?

The opentheory tool processes higher order logic theory packages.

Features of the opentheory tool

• Coded in Standard ML (SML), and ported to the MLton, Poly/ML and Moscow ML compilers.
• The opentheory tool is used to power the OpenTheory project.

Project status

The opentheory tool is being actively developed: the latest version is opentheory 1.4 (release 20230321). The opentheory tool is free software, released under the MIT License. To adapt the opentheory tool 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.