A Theorem-Proving Language for Experimentation 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 extend ability will permit general experimentation with the various alternative systems. CACM June, 1974 Henschen, L. Overbeek, R. Wos, L. theorem proving, resolution, factoring, paramodulation, programming languages 3.60 4.22 5.21 CA740602 JB January 17, 1978 3:37 PM 2644 5 2644 2644 5 2644 2644 5 2644