A Theorem-Proving Language for Experimentation

Lawrence Joseph Henschen, Ross Overbeck, L. Wos

Research output: Contribution to journalArticlepeer-review


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.

Original languageEnglish (US)
Pages (from-to)308-314
Number of pages7
JournalCommunications of the ACM
Issue number6
StatePublished - Jun 1 1974


  • factoring
  • paramodulation
  • programming languages
  • resolution
  • theorem proving

ASJC Scopus subject areas

  • Computer Science(all)


Dive into the research topics of 'A Theorem-Proving Language for Experimentation'. Together they form a unique fingerprint.

Cite this