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.

REFERENCES

• 1: CHINLUND, T., DAVIS, M., HTINMAN, P ., AND MCILROY, M. D. Theorem-proving by matching. Submitted for publication.
• 2: DAvis, M. ELiminating the irrelevant from mechanical proofs. Proc. Syrup. Appl. Math. XV (1963), 15-30.
• 3: Joyce Friedman, A Semi-Decision Procedure for the Functional Calculus, Journal of the ACM (JACM), v.10 n.1, p.1-24, Jan. 1963 [doi>10.1145/321150.321151]
• 4: PRAWITZ, D. An improved proof procedure. Theoria 26 (1960), 102-139.
• 5: QUINE, W.V. A proof procedure for quantification theory. J. Symbolic Logic 20 (1955), 141-149.
• 6: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 7: Wos, L., CARSON, D., AND IOBINSON, G. The unit preference strategy in theorem provbig. Proc. AFIPS 1964 Fall Joint Comput. Conf., Vol. 26, Pt. II, pp. 615-621 (Spartan Books, Washington, I). C.).
• 8: Lawrence Wos , George A. Robinson , Daniel F. Carson, Efficiency and Completeness of the Set of Support Strategy in Theorem Proving, Journal of the ACM (JACM), v.12 n.4, p.536-541, Oct. 1965 [doi>10.1145/321296.321302]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Algorithms, Languages, Measurement, Performance, Theory, Verification