Z-Resolution: Theorem-Proving with Compiled Axioms

ABSTRACT

An improved procedure for resolution theorem proving, called Z-resolution, is described. The basic idea of Z-resolution is to “compile” some of the axioms in a deductive problem. This means to automatically transform the selected axioms into a computer program which carries out the inference rules indicated by the axioms. This is done automatically by another program called the specializer. The advantage of doing this is that the compiled axioms run faster, just as a compiled program runs faster than an interpreted program. A proof is given that the inference rule used in Z-resolution is complete, provided that the axioms “compiled” have certain properties.

REFERENCES

• 1: BERKELEY, E.C et al The programming language "LISP": Its operation and applications. Information International, Inc., Maynard, Mass., 1964.
• 2: Daniel G. Bobrow , Daniel L. Murphy, Structure of a LISP system using two-level storage, Communications of the ACM, v.10 n.3, p.155-159, March 1967 [doi>10.1145/363162.363185]
• 3: DARLINGTON, J.L. Automatic theorem proving with equahty substitutions and mathematical induction. In Machine Intelligence 3, Edinburgh U. Press, Edinburgh, 1968, pp. 113-127.
• 4: John Kent Dixon, An improved method for solving deductive problems on a computer by compiled axioms, 1970
• 5: DIXON, J. K. The specializer. A method of automatically writing computer programs (to be submitted for publication).
• 6: DixoN, J.K. Experiments with a Z-resolution program (to be submitted for publication).
• 7: Bert F. Green, Jr. , Alice K. Wolf , Carol Chomsky , Kenneth Laughery, Baseball: an automatic question answerer, Computers & thought, MIT Press, Cambridge, MA, 1995
• 8: KLEENE, S. C. Mathematical Logic. Wiley, New York, 1967.
• 9: LOMBARDI, L. A., AND RAPHAEL, B. LISP as the language for an incremental computer. In The Programming Language LISP: Its Operatwn and Applications. MIT Press, Cambridge, Mass., 1964, pp. 204-220.
• 10: John McCarthy, LISP 1.5 Programmer's Manual, The MIT Press, 1962
• 11: MORRIS, J. B. E-resolution: Extension of resolution to include the equality relation. Proc. Internat. Joint Conf on Artificial Intelligence, 1969
• 12: QUAM, L. It. Stanford LISP 1.6 Manual. Stanford U. Artificial Intelligence Prog., Stanford, Calif., Dec. 31, 1968.
• 13: 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]
• 14: :ROBINSON, G., AND WOS, L. Paramodulation and theorem-proving in first-order theories with equality, in Machine intelhgeuce 4, B. Meltzer and D M~chie, Eds., Edinburgh U Press, Edinburgh, 1969, pp. 135-150.
• 15: SIBERT, E.E. A Machine-oriented logic incorporating the equality relation. In Machine Intelhgence 4, B Meltzer and D. Michie, Eds, Edinburgh U. Press, Edinburgh, 1969 pp. 163-134.
• 16: SANDEWALL, E. J. LISP A: A LISP-like system for incremental computing. Proc. AFIPS 1968 SJCC, Vol. 32, AFIPS Press, Montvale, N J., pp. 375-384.
• 17: James R. Slagle, Automatic Theorem Proving With Renamable and Semantic Resolution, Journal of the ACM (JACM), v.14 n.4, p.687-697, Oct. 1967 [doi>10.1145/321420.321428]
• 18: WmSSMAN, C. LISP 1 5 Primer Dickerson Pub. Co., Belmont, Calif., 1967.
• 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]
• 20: Lawrence Wos , George A. Robinson , Daniel F. Carson , Leon Shalla, The Concept of Demodulation in Theorem Proving, Journal of the ACM (JACM), v.14 n.4, p.698-709, Oct. 1967 [doi>10.1145/321420.321429]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers

Additional Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE

General Terms:
Experimentation, Languages, Performance, Theory, Verification