IMPS is an Interactive Mathematical Proof System developed by W. M. Farmer, J. D. Guttman, and F. J. Thayer at The MITRE Corporation during 1990-1993. It is intended to provide mechanical support for traditional mathematical techniques and styles of practice. The system consists of a library of mathematics plus facilities for developing axiomatic theories, proving conjectures, and performing rigorous symbolic computations. It is available under a BSD-like free license.

Home page:



Theorem Provers