Mechanical Theorem-Proving by Model Elimination

Abstract

A proof procedure based on a theorem of Herbrand and utilizing the matching technique of Prawitz is presented. In general, Herbrand-type proof procedures proceed by generating over increasing numbers of candidates for the truth-functionally contradictory statement the procedures seek. A trial is successful when some candidate is in fact a contradictory statement. In procedures to date the number of candidates developed before a contradictory statement is found (if one is found) varies roughly exponentially with the size of the contradictory statement. (“Size” might be measured by the number of clauses in the conjunctive normal form of the contradictory statement.) Although basically subject to the same rate of growth, the procedure introduced here attempts to drastically trim the number of candidates at an intermediate level of development. This is done by retaining beyond a certain level only candidates already “partially contradictory.” The major task usually is finding the partially contradictory sets. However, the number of candidate sets required to find these subsets of the contradictory set is generally much smaller than the number required to find the full contradictory set.