What is opentheory?

opentheory is a tool for processing higher order logic theories.

Features of opentheory

• Coded in Standard ML (SML), and ported to the MLton, Poly/ML and Moscow ML compilers.
• Processes higher order logic theories in the proof article file format of the OpenTheory project.

Project Status

The latest version is opentheory 1.0 (release 20090617), released under version 2 of the GNU General Public Licence. The program is used to power the OpenTheory project.

Contact

To report bugs, request features, or obtain help using opentheory, please email joe@gilith.com