Theorem Proving by Covering Expressions

Lawrence Joseph Henschen*

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

5 Scopus citations


This paper presents a reformulation of Gilmore's approach Rather than generate instances by saturation, the authors start with a few instances, convert to a nonredundant disjunctive normal form (DNF), and then use that DNF to help grade the choice of further instances The DNF in essence represents m a convenient form all the Boolean relations of the hteral instances Viewed differently, the DNF provides a concise description of clauses which, ffadded, would produce unsatlsfiablhty Thus the mare activity in the theorem-proving process Js analyzing possible new instances of input clauses and their relationship to the already present instances Some examples from an interactive program are given.

Original languageEnglish (US)
Pages (from-to)385-400
Number of pages16
JournalJournal of the ACM (JACM)
Issue number3
StatePublished - Jul 1 1979


  • artificial intelligence
  • logic covering expressions
  • resolution
  • semantic trees
  • theorem proving

ASJC Scopus subject areas

  • Control and Systems Engineering
  • Software
  • Information Systems
  • Hardware and Architecture
  • Artificial Intelligence


Dive into the research topics of 'Theorem Proving by Covering Expressions'. Together they form a unique fingerprint.

Cite this