A Theorem-Proving Language for Experimentation
Copyright © 1974, Association for Computing Machinery, Inc. General permission to republish, but not for profit, all or part of this material is granted provided that ACM's copyright notice is given and that reference is made to the publication, to its date of issue, and to the fact that reprinting privileges were granted by permission of the Association for Computing Machinery.
Work performed under the auspices of the United States Atomic Energy Commission and supported in part by the National Science Foundation under grants GJ-32717 and GJ-35721.
Reprinted with permission from the Communications of the Association for Computing Machinery, Vol. 17, no. 6, pp. 308-314 (June 1974).
Because of the large number of strategies and inference rules presently under consideration in automated theorem proving, there is a need for developing a language especially oriented toward automated theorem proving. This paper discusses some of the features and instructions of this language. The use of this language permits easy extension of automated theorem-proving programs to include new strategies and/or new inference rules. Such extendability will permit general experimentation with the various alternative systems.
