A Human Oriented Logic for Automatic Theorem-Proving

ABSTRACT

A deductive system is described which combines aspects of resolution (e.g. unification and the use of Skolem functions) with that of natural deduction and whose performance compares favorably with the best predicate calculus theorem provers.

REFERENCES

• 1: ALLEN, JOHN, AND LUCKHAM, DAVID. An interactive theorem proving program. In Machine Intelligence 5. B. Meltzer and D. Michie, Eds., Edinburgh. U. Press, Edinburgh, 1970, pp. 321- 336.
• 2: BLEgSOE, W.W. Splitting and reduction heuristics in automatic theorem proving. Artif. Intel. 2 (Spring 1971), 55-77.
• 3: BLEDSOE, W. W., BOYER, ROBERT S., AND HENNEMAN, WILLIAM I~. Computer proofs of limit theorems. Artif. Intel. 3 (Spring 1972), 27-60.
• 4: C. L. Chang, The Unit Proof and the Input Proof in Theorem Proving, Journal of the ACM (JACM), v.17 n.4, p.698-707, Oct. 1970 [doi>10.1145/321607.321618]
• 5: CHANG, C. L. Theorem proving with variable-constrained resolution. Inform. Sciences $, 3 (July 1972), 217-231.
• 6: CHINTHAYAMMA. Sets of independent axioms for a ternary Boolean algebra. Notices Amer. Math. Soc. 16, 4 (June 1969), 69T-A69, 654.
• 7: ERNST, GF~OaGF~ W. The utility of independent subgoals in theorem proving. Inform. and Contr. 18, 3 (April 1971), 237-252.
• 8: KLEENE, STEPHEN C. Introduction to Metamathematics. Van Nostrand, Princeton, N.J., 1952.
• 9: KOWALSKI, ROBERT, AND KUEHNER, DAVID. Linear resolution with selection function. Artif. Intel. 2 (Winter 1971), 227-260.
• 10: D. W. Loveland, A Unifying View of Some Linear Herbrand Procedures, Journal of the ACM (JACM), v.19 n.2, p.366-384, April 1972 [doi>10.1145/321694.321706]
• 11: MORRIS, jAMES B. E-resolution: Extension of resolution to include the equality relation. Proc. int. Joint Conf. Artificial Intelligence, Washington, D.C., 1989, pp. 287-294.
• 12: Nils J. Nilsson, Problem-Solving Methods in Artificial Intelligence, McGraw-Hill Pub. Co., 1971
• 13: NORTON, LEWIS M. Experiments with a heuristic theorem-proving program for predicate calculus with equality. Artif. Intel. 2 (Winter 1971), 261-284.
• 14: ROBINSON, GEORGE, AND WOS, LAWRENCE. Paramodulation and theorem-proving in first order theories with equality. In Machine Intelligence 4, B. Meltzer and D. Michie, Eds., Edinburgh U. Press, Edinburgh, 1969, pp. 135-150.
• 15: J. A. Robinson, Theorem-Proving on the Computer, Journal of the ACM (JACM), v.10 n.2, p.163-174, April 1963 [doi>10.1145/321160.321166]
• 16: 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]
• 17: Claude E. Shannon , Warren Weaver, A Mathematical Theory of Communication, University of Illinois Press, Champaign, IL, 1963
• 18: SLAGLE, JAMES R., AND KONIVER, DEENA A. Finding resolution graphs and using duplicate goals in AND/OR trees. Inform. Sciences 3, 4 (Oct. 1971), 315-342.
• 19: 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:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming

General Terms:
Human Factors, Theory, Verification