Journal article
IMPS: An interactive mathematical proof system
Abstract
IMPS is an interactive mathematical proof system intended as a general-purpose tool for formulating and applying mathematics in a familiar fashion. The logic of IMPS is based on a version of simple type theory with partial functions and subtypes. Mathematical specification and inference are performed relative to axiomatic theories, which can be related to one another via inclusion and theory interpretation. IMPS provides relatively large …
Authors
Farmer WM; Guttman JD; Thayer FJ
Journal
Journal of Automated Reasoning, Vol. 11, No. 2, pp. 213–248
Publisher
Springer Nature
Publication Date
June 1993
DOI
10.1007/bf00881906
ISSN
0168-7433