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