IMPS, an Interactive Mathematical Proof System [2], is intended as a general purpose tool for formulating and applying mathematics in a familiar fashion. Its logic is a conceptually simple implementation of higher-order predicate logic that closely conforms to mathematical practice. Mathematical specification and inference are performed relative to axiomatic theories, which can be combined with each other and extended by definitions. The system supports a natural style of inference based on deduction graphs, which are akin to derivations in a sequent calculus. However, the individual inferences in a deduction graph may depend on theory-specific simplification procedures, and may encapsulate a large number of basic inferences.
CITATION STYLE
Farmer, W. M., Guttman, J. D., & Thayer, F. J. (1990). IMPS: An interactive mathematical proof system. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 449 LNAI, pp. 653–654). Springer Verlag. https://doi.org/10.1007/3-540-52885-7_126
Mendeley helps you to discover research relevant for your work.