THEOREM PROVING BY COVERING EXPRESSIONS

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. © 1979, ACM. All rights reserved.