Special relations in automated deduction

ABSTRACT

Two deduction rules are introduced to give streamlined treatment to relations of special importance in an automated theorem-proving system. These rules, the relation replacement and relation matching rules, generalize to an arbitrary binary relation the paramodulation and E-resolution rules, respectively, for equality, and may operate within a nonclausal or clausal system. The new rules depend on an extension of the notion of polarity to apply to subterms as well as to subsentences, with respect to a given binary relation. The rules allow us to eliminate troublesome axioms, such as transitivity and monotonicity, from the system; proofs are shorter and more comprehensible, and the search space is correspondingly deflated.

REFERENCES

• 1: ANDERSON, R. Completeness results for E-resolution. In Proceedings of AFIPS Spring Joint Computer Conference. AFIPS Press, Reston, Va., 1970, 652-656.
• 2: BOYER, R. S. AND MOORE, J.S. A Computational Logic. Academic Press, Orlando, Fla., 1979.
• 3: BRAND, D. Proving theorems with the modification method. SlAM J. Comput. 4, 2 (1975), 412-430.
• 4: Chin-Liang Chang , Richard C. Lee , Richard Char-Tung Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, Inc., Orlando, FL, 1997
• 5: Vincent Joseph Digricoli, Resolution by unification and equality, 1983
• 6: Robert Kowalski, Logic for problem-solving, North-Holland Publishing Co., Amsterdam, The Netherlands, 1986
• 7: LOVELAND, D. W. Automated Theorem Proving: A Logical Basis. North-Holland, New York, 1978.
• 8: Zohar Manna , Richard Waldinger, A Deductive Approach to Program Synthesis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.1, p.90-121, Jan. 1980 [doi>10.1145/357084.357090]
• 9: MANNA, Z. AND WALDINGER, R. Deductive synthesis of the unification algorithm. Sci. Comput. Prog. 1 ( 1981 ), 5-48.
• 10: MANNA, Z., AND WALDINGER, R. Special relations in program-synthetic deduction. Tech. Rep. Comput. Sci. Dept., Stanford Univ., Stanford, Calif., and Artificial Intelligence Center, SRI International, Menlo Park, Calif., March 1982.
• 11: Zohar Manna , Richard Waldinger, The logical basis for computer programming. Volume 1: deductive reasoning, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1985
• 12: Zohar Manna , Richard Waldinger, The logical basis for computer programming: vol. 2, deductive systems, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 13: MANNA, Z., AND WALDINGER, R. The origin of the binary-search paradigm, in Proceedings ofthe 9th International Joint Conference on Artificial Intelligence (Los Angeles, Calif., Aug. 18-23). Morgan-Kaufman Publishing, Los Altos, Calif., 1985, pp. 222-224.
• 14: MORRIS, J.B. E-resolution: Extension of resolution to include the equality relation. In Proceedings of the International Joint Conference on Artificial Intelligence (Washington, DC, May 7-9). 1969, pp. 287-294.
• 15: MURRAY, N.V. Completely nonclausal theorem proving. Artif Intell. 18, 1 (1982), 67-85.
• 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: ROmNSON, J.A. Logic." Form and Function. North-Holland, New York, 1979.
• 18: STICKEL, M.E. A nonclausal connection-graph resolution theorem-proving program. In Proceedings of the National Conference on Artificial Intelligence (Pittsburgh, Pa., Aug. 18-20). American Association for Artificial Intelligence, Menlo Park, Calif., 1982, pp. 229-233.
• 19: TRAUGOTT, J. Deductive synthesis of sorting algorithms. Tech. Rep. Comput. Sci. Dept., Stanford Univ., Stanford, Calif. (forthcoming).
• 20: Wos, L., AND ROBINSON, G. Paramodulation and theorem proving in first order theories with equality. In Machine Intelligence, vol 4, B. Meltzer and D. Michie, Eds. American Elsevier, New York, 1969, pp. 135-150.

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: Mechanical theorem proving

General Terms:
Algorithms, Theory, Verification