Theorem proving using equational matings and rigid E-unification

ABSTRACT

In this paper, it is shown that the method of matings due to Andrews and Bibel can be extended to (first-order) languages with equality. A decidable version of E-unification called rigid E-unification is introduced, and it is shown that the method of equational matings remains complete when used in conjunction with rigid E-unification. Checking that a family of mated sets is an equational mating is equivalent to the following restricted kind of E-unification. Problem Given E&ar;=Ei∣ 1≤i≤n a family of n finite sets of equations and S=ui,vi ∣1≤i≤n a set of n pairs of terms, is there a substitution q such that, treating each set qEi as a set of ground equations (i.e., holding the variables in qEi “rigid”), qui , and qvi are provably equal from qEi for i=1,...,n ? Equivalently, is there a substitution q such that qui and qvi can be shown congruent from qEi by the congruence closure method for i=1,...,n ? A substitution q solving the above problem is called a rigid E&ar; -unifier of S, and a pair E&ar;,S such that S has some rigid E&ar; -unifier is called an equational premating. It is show that deciding whether a pair E&ar;,S is an equational premating is an NP-complete problem.

REFERENCES

• 1: Peter B. Andrews, Theorem Proving via General Matings, Journal of the ACM (JACM), v.28 n.2, p.193-214, April 1981 [doi>10.1145/322248.322249]
• 2: Peter B. Andrews, An introduction to mathematical logic and type theory: to truth through proof, Academic Press Professional, Inc., San Diego, CA, 1986
• 3: ANDREWS, P. B., MILLER, D., COMEN, E., AND PFENYING, F. Automating higher-order logic, Contemp. Math. 29, (1984), 169-192.
• 4: Leo Bachmair , Ronald V. Book, Canonical Equational Proofs, Birkhauser, 1991
• 5: BACHMAIR, L., DERSHOWITZ, N., AND PLAISTED, D. Completion without failure. In Resohtion of Equatzons in Algebraic Structures, vol. 2. In A'it-Kaci and Nivat, eds. Academic Press, 1989, pp. 1-30,
• 6: BACHMAIR, L., DERSHOWtTZ, N., AND HSJANG, J. Orderings for equational proofs, In Logzc in Computer Science (LICS'86) (Cambridge, Mass., June 16~18). IEEE, New York, 1986, pp. 346-357.
• 7: B~BEt, W. Tautology testing with a generalized matrix reduction method. Theoret. Comput. Sci. 8 (1979), 31-44.
• 8: Wolfgang Bibel, On Matrices with Connections, Journal of the ACM (JACM), v.28 n.4, p.633-645, Oct. 1981 [doi>10.1145/322276.322277]
• 9: BtBEL, W. Automated Theorem ProL~ing. Friedrich Vieweg & Sohn, Braunschweig, Germany, 1982.
• 10: BIBEL, W., AND SCHREIBER, J. Proof search in a Gentzen-like system of first-order logic. In Proceedings of the International Computing Symposmm. North-Holland, Amsterdam, 1975, pp. 205-212.
• 11: Nachum Dershowitz, Termination of rewriting, Journal of Symbolic Computation, v.3 n.1-2, p.69-116, Feb./April 1987 [doi>10.1016/S0747-7171(87)80022-6]
• 12: Nachum Dershowitz , Leo Marcus , Andrzej Tarlecki, Existence, uniqueness, and construction of rewrite systems, SIAM Journal on Computing, v.17 n.4, p.629-639, August 1988 [doi>10.1137/0217039]
• 13: Peter J. Downey , Ravi Sethi , Robert Endre Tarjan, Variations on the Common Subexpression Problem, Journal of the ACM (JACM), v.27 n.4, p.758-771, Oct. 1980 [doi>10.1145/322217.322228]
• 14: Elmar Eder, A Comparison of the Resolution Caculus and the Connection Method, and a new Calculus Generalizing Both Methods, Proceedings of the 2nd Workshop on Computer Science Logic, p.80-98, October 03-07, 1988
• 15: Elmar Eder, Relative complexities of first order calculi, Verlag Vieweg, Wiesbaden, Germany, 1992
• 16: FJTTING, M. A tableaux based automated theorem prover for classical logic. Tech. Rep. City Univ. of New York, New York, June 1986.
• 17: Jean H. Gallier, Logic for computer science: foundations of automatic theorem proving, Harper & Row Publishers, Inc., New York, NY, 1985
• 18: GALLIER, J. H., RAATZ, S., AND SNYDER, W. Theorem proving using rigid E-unification: Equational matings. In Logic bz Computer Science (LICS'87) (Ithaca, N.Y.). IEEE, New York, t987, pp. 338-346.
• 19: GALLIER, J. H., NARENDRAN, P., PLAISTED, D., RAATZ, S., AND SNYDER, W. Finding canonical rewriting systems equivalent to a finite set of ground equations in polynomial time. J. A CM, to appear.
• 20: GALLIER, J. H., NARENDRAN, P., PLAISTED, D., AND SNYDER, W. Rigid E-unification is NP-complete. In Logtc m Computer Science (LICS'88)(Edinburgh, Scotland, July 5-8). IEEE, New York, 1988, pp. 2t8-227.
• 21: J. H. Gallier , W. Snyder, Complete sets of transformations for general E-unification, Theoretical Computer Science, v.67 n.2-3, p.203-260, Oct. 1989 [doi>10.1016/0304-3975(89)90004-2]
• 22: Jean Gallier , Paliath Narendran , David A. Plaisted , Wayne Snyder, Rigid E-unification: NP-completeness and applications to equational matings, Information and Computation, v.87 n.1-2, p.129-195, July/August 1990 [doi>10.1016/0890-5401(90)90061-L]
• 23: Jean-Yves Girard, Linear logic, Theoretical Computer Science, v.50 n.1, p.1-102, Jan. 30, 1987 [doi>10.1016/0304-3975(87)90045-4]
• 24: HERBRAND, J. Logical Writings. Reidel Publishing Company, Hingham, Mass., 197i.
• 25: HUF, T, G. A unification algorithm for typed A-calculus. Theor. Comp. Scz. I (1975), 27-57.
• 26: HUET, G. Rdsolution d'Equations dans les Langages d'Ordre 1, 2 w. Th6se d'Etat, Universit6 de Paris VII, Paris, France, 1976.
• 27: Gérard Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM (JACM), v.27 n.4, p.797-821, Oct. 1980 [doi>10.1145/322217.322230]
• 28: HUET, G., AND OPPEN, D.C. Equations and rewrite rules: A survey. In R. V. Book, ed., Formal Languages: Perspectives and Open Problems. Academic Press, Orlando, Fla., 1982, pp. 349-405.
• 29: KNUTH, D. E., AND BENDIX, P.B. Simple word problems in universal algebras. In J. Leech, ed., Computational Problems in Abstract Algebra, Pergamon Press, 1970, pp. 263-297.
• 30: Dexter Kozen, Complexity of Finitely Presented Algebras, Cornell University, Ithaca, NY, 1976
• 31: KOZ~N, D. Positive first-order logic is NP-complete. IBMJ. Res. Dec'. 25, 4 (1981), 327-332.
• 32: LEVY, A. Basic Set Theopy. Springer-Verlag, New York, 1979.
• 33: Alberto Martelli , Ugo Montanari, An Efficient Unification Algorithm, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.2, p.258-282, April 1982 [doi>10.1145/357162.357169]
• 34: MET~WF.r~, Y. About the rewriting systems produced by the Knuth-Bendix completion algorithm. Inf. Proc. Lett. 16 (1983), 31-34.
• 35: Dale Miller, Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs, Proceedings of the 7th International Conference on Automated Deduction, p.375-393, May 14-16, 1984
• 36: Greg Nelson , Derek C. Oppen, Fast Decision Procedures Based on Congruence Closure, Journal of the ACM (JACM), v.27 n.2, p.356-364, April 1980 [doi>10.1145/322186.322198]
• 37: PATERSON, M. S., AND WEGMAN, M.N. Linear unification. J. Comput. Syst. Sci. 16 (1978), 158-167.
• 38: PFENNING, F. Proof transformations in higher-order logic. Ph.D. dissertation. Department of Mathematics, Carnegie Mellon Univ., Pittsburgh, Pa., Jan. 1987.
• 39: PLOTKIN, G. Building in equational theories. Machine Intelligence 7 (1972), 73-90.
• 40: SMULLYAN, R.M. First-order Logic. Springer-Verlag, New York, 1968.
• 41: SZABO, M. E. The collected papers of Gerhard Gentzen. In: Studies in Logic. Elsevier North-Holland, New York, 1970.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.3 Complexity Measures and Classes
          Subjects: Reducibility and completeness

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Complexity of proof procedures
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Proof theory; Computational logic; Mechanical theorem proving

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.2 Algorithms
          Subjects: Algebraic algorithms
      I.1.3 Languages and Systems
          Subjects: Special-purpose algebraic systems
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Deduction (e.g., natural, rule-based); Metatheory**

General Terms:
Algorithms, Languages, Performance, Theory

Keywords:
Knuth-Bendix procedure, NP-completeness, automated theorem proving, equational reasoning, matings, unification