Theorem Proving by Covering Expressions

Lawrence Joseph Henschen*

*Corresponding author for this work

Research output: Contribution to journalArticle

5 Scopus citations

Abstract

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)
Volume26
Issue number3
DOIs
StatePublished - Jul 1 1979

Keywords

  • 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

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

  • Cite this