Skip to main content
SpringerLink
Log in

What you always wanted to know about rigid E-unification

  • Automated Reasoning
  • Conference paper
  • First Online:
Logics in Artificial Intelligence (JELIA 1996)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1126))

Included in the following conference series:

Abstract

This paper solves an open problem posed by a number of researchers: the construction of a complete calculus for matrix-based methods with rigid E-unification. The use of rigid E-unification and simultaneous rigid E-unification for such methods has been proposed by Gallier, Raatz and Snyder [35]. After our proof of the undecidability of simultaneous rigid E-unification [22] it has become clear that one should look for more refined techniques to deal with equality in matrix-based methods. In this article, we define a complete proof procedure for firstorder logic with equality based on an incomplete but terminating procedure for rigid E-unification. Our approach is applicable to the connection method and the tableau method and illustrated on the tableau method.

Supported by a grant from the Swedish Royal Academy of Sciences.

Supported by a TFR grant.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P.B. Andrews. Theorem proving via general matings. Journal of the Association for Computing Machinery, 28(2):193–214, 1981.

    Google Scholar 

  2. A. Avron. Gentzen-type systems, resolution and tableaux. Journal of Automated Reasoning, 10:256–281, 1993.

    Article  Google Scholar 

  3. L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basic paramodulation and superposition. In D. Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 462–476, Saratoga Springs, NY, USA, June 1992. Springer Verlag.

    Google Scholar 

  4. L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basis paramodulation. Information and Computation, 121:172–192, 1995.

    Article  Google Scholar 

  5. Peter Baumgartner. An ordered theory resolution calculus. In A. Voronkov, editor, Logic Programming and Automated Reasoning (LPAR'92), volume 624 of Lecture Notes in Computer Science, pages 119–130, 1992.

    Google Scholar 

  6. P. Baumgartner and U. Furbach. Consolution as a framework for comparing calculi. Journal of Symbolic Computations, 16:445–477, 1993.

    Article  Google Scholar 

  7. P. Baumgartner and U. Furbach. PROTEIN: A PROver with a Theory Extension INterface. In A. Bundy, editor, Automated Deduction — CADE-12. 12th International Conference on Automated Deduction., volume 814 of Lecture Notes in Artificial Intelligence, pages 769–773, Nancy, France, June/July 1994.

    Google Scholar 

  8. G. Becher and U. Petermann. Rigid unification by completion and rigid paramodulation. In B. Nebel and L. Dreschler-Fischer, editors, KI-94: Advances in Artificial Intelligence. 18th German Annual Conference on Artificial Intelligence, volume 861 of Lecture Notes in Artificial Intelligence, pages 319–330, Saarbrücken, Germany, September 1994. Springer Verlag.

    Google Scholar 

  9. B. Beckert. A completion-based method for mixed universal and rigid E-unification. In A. Bundy, editor, Automated Deduction — CADE-12. 12th International Conference on Automated Deduction., volume 814 of Lecture Notes in Artificial Intelligence, pages 678–692, Nancy, France, June/July 1994.

    Google Scholar 

  10. B. Beckert. Are minimal solutions to simultaneous rigid E-unification sufficient for adding equality to semantic tableaux? Privately circulated manuscript, University of Karlsruhe, 1995.

    Google Scholar 

  11. B. Beckert and R. Hähnle. An improved method for adding equality to free variable semantic tableaux. In D. Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 678–692, Saratoga Springs, NY, USA, June 1992. Springer Verlag.

    Google Scholar 

  12. W. Bibel. On matrices with connections. Journal of the Association for Computing Machinery, 28(4):633–645, 1981.

    Google Scholar 

  13. W. Bibel. Issues in theorem proving based on the connection method. In P. Baumgartner, R. Hähnle, and J. Posegga, editors, Theorem Proving with Analytic Tableaux and Related Methods, number 918 in Lecture Notes in Artificial Intelligence, pages 1–16, Schloß Rheinfels, St. Goar, Germany, May 1995.

    Google Scholar 

  14. D. Brand. Proving theorems with the modification method. SIAM Journal of Computing, 4:412–430, 1975.

    Article  Google Scholar 

  15. C.L. Chang. Theorem proving with variable-constrained resolution. Information Sciences, 4:217–231, 1972.

    Google Scholar 

  16. A. Degtyarev. The strategy of monotone paramodulation (in Russian). In Fifth Soviet All-Union Conference on Mathematical Logic, page 39, Novosibirsk, 1979.

    Google Scholar 

  17. A. Degtyarev. On the forms of inference in calculi with equality and paramodulation (in Russian). In Yu.V. Kapitonova, editor, Automation of Research in Mathematics, pages 14–26. Institute of Cybernetics, Kiev, 1982.

    Google Scholar 

  18. A. Degtyarev, Yu. Matiyasevich, and A. Voronkov. Simultaneous rigid E-unification and related algorithmic problems. To appear in LICS'96, 9 pages, 1996.

    Google Scholar 

  19. A. Degtyarev and A. Voronkov. Equality elimination for semantic tableaux. UPMAIL Technical Report 90, Uppsala University, Computing Science Department, December 1994. To appear in DISCO'96.

    Google Scholar 

  20. A. Degtyarev and A. Voronkov. General connections via equality elimination. UPMAIL Technical Report 93, Uppsala University, Computing Science Department, January 1995.

    Google Scholar 

  21. A. Degtyarev and A. Voronkov. Simultaneous rigid E-unification is undecidable. UPMAIL Technical Report 105, Uppsala University, Computing Science Department, May 1995. To appear in Theoretical Computer Science, v.166, 1996.

    Google Scholar 

  22. A. Degtyarev and A. Voronkov. Reduction of second-order unification to simultaneous rigid E-unification. UPMAIL Technical Report 109, Uppsala University, Computing Science Department, June 1995.

    Google Scholar 

  23. A. Degtyarev and A. Voronkov. General connections via equality elimination. In M. De Glas and Z. Pawlak, editors, Second World Conference on the Fundamentals of Artificial Intelligence (WOCFAI-95), pages 109–120, Paris, July 1995. Angkor.

    Google Scholar 

  24. A. Degtyarev and A. Voronkov. Equality elimination for the inverse method and extension procedures. In C.S. Mellish, editor, Proc. International Joint Conference on Artificial Intelligence (IJCAI), volume 1, pages 342–347, Montréal, August 1995.

    Google Scholar 

  25. A. Degtyarev and A. Voronkov. Handling equality in logic programs via basic folding. In R. Dyckhoff, H. Herre, and P. Schroeder-Heister, editors, Extensions of Logic Programming (5th International Workshop, ELP'96), volume 1050 of Lecture Notes in Computer Science, pages 119–136, Leipzig, Germany, March 1996.

    Google Scholar 

  26. A. Degtyarev and A. Voronkov. Decidability problems for the prenex fragment of intuitionistic logic. To appear in LICS'96, 10 pages, 1996.

    Google Scholar 

  27. A. Degtyarev and A. Voronkov. What you always wanted to know about rigid E-unification. UPMAIL Technical Report, Uppsala University, Computing Science Department, to appear.

    Google Scholar 

  28. E. De Kogel. Rigid E-unification simplified. In P. Baumgartner, R. Hähnle, and J. Posegga, editors, Theorem Proving with Analytic Tableaux and Related Methods, number 918 in Lecture Notes in Artificial Intelligence, pages 17–30, Schloß Rheinfels, St. Goar, Germany, May 1995.

    Google Scholar 

  29. E. Eder. A comparison of the resolution calculus and the connection method, and a new calculus generalizing both methods. In E. Börger, G. Jäger, H. Kleine Büning, and M.M. Richter, editors, CSL'88 (Proc. 2nd Workshop on Computer Science Logic), volume 385 of Lecture Notes in Computer Science, pages 80–98. Springer Verlag, 1988.

    Google Scholar 

  30. E. Eder. Consolution and its relation with resolution. In Proc. International Joint Conference on Artificial Intelligence (IJCAI), pages 132–136, 1991.

    Google Scholar 

  31. M. Fitting. First Order Logic and Automated Theorem Proving. Springer Verlag, New York, 1990.

    Google Scholar 

  32. J. Gallier, P. Narendran, D. Plaisted, and W. Snyder. Rigid E-unification: NP-completeness and applications to equational matings. Information and Computation, 87(1/2):129–195, 1990.

    Article  Google Scholar 

  33. J. Gallier, P. Narendran, S. Raatz, and W. Snyder. Theorem proving using equational matings and rigid E-unification. Journal of the Association for Computing Machinery, 39(2):377–429, 1992.

    Google Scholar 

  34. J.H. Gallier, P. Narendran, D. Plaisted, and W. Snyder. Rigid E-unification is NP-complete. In Proc. IEEE Conference on Logic in Computer Science (LICS), pages 338–346. IEEE Computer Society Press, July 1988.

    Google Scholar 

  35. J.H. Gallier, S. Raatz, and W. Snyder. Theorem proving using rigid E-unification: Equational matings. In Proc. IEEE Conference on Logic in Computer Science (LICS), pages 338–346. IEEE Computer Society Press, 1987.

    Google Scholar 

  36. J.H. Gallier, S. Raatz, and W. Snyder. Rigid E-unification and its applications to equational matings. In H. Aït Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, volume 1, pages 151–216. Academic Press, 1989.

    Google Scholar 

  37. J. Goubault. A rule-based algorithm for rigid E-unification. In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors, Computational Logic and Proof Theory. Proceedings of the Third Kurt Gödel Colloquium, KGC'93, volume 713 of Lecture Notes in Computer Science, pages 202–210, Brno, August 1993.

    Google Scholar 

  38. J. Goubault. Rigid E-unifiability is DEXPTIME-complete. In Proc. IEEE Conference on Logic in Computer Science (LICS). IEEE Computer Society Press, 1994.

    Google Scholar 

  39. R. Hähnle, B. Beckert, and S. Gerberding. The many-valued tableau-based theorem prover 3 T AP. Technical Report 30/94, Universität Karlsruhe, Fakultät für Informatik, November 1994.

    Google Scholar 

  40. S. Kanger. A simplified proof method for elementary logic. In J. Siekmann and G. Wrightson, editors, Automation of Reasoning. Classical Papers on Computational Logic, volume 1, pages 364–371. Springer Verlag, 1983. Originally appeared in 1963.

    Google Scholar 

  41. J. Kruskal. Well quasi ordering, the tree problem and Vazsonyi's conjecture. Transactions of the American Mathematical Society, 95:210–225, 1960.

    Google Scholar 

  42. R.C.T. Lee and C.L. Chang. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.

    Google Scholar 

  43. D.W. Loveland. Mechanical theorem proving by model elimination. Journal of the Association for Computing Machinery, 15:236–251, 1968.

    Google Scholar 

  44. D.W. Loveland. Automated Theorem Proving: a Logical Basis. North Holland, 1978.

    Google Scholar 

  45. S.Yu. Maslov. The inverse method of establishing deducibility in the classical predicate calculus. Soviet Mathematical Doklady, 5:1420–1424, 1964.

    Google Scholar 

  46. S.Yu. Maslov. An invertible sequential variant of constructive predicate calculus (in Russian). Zapiski Nauchnyh Seminarov LOMI, 4, 1967. English Translation in: Seminars in Mathematics: Steklov Math. Inst. 4, Consultants Bureau, NY-London, 1969, p. 36–42.

    Google Scholar 

  47. V.A. Matulis. On variants of classical predicate calculus with the unique deduction tree (in Russian). Soviet Mathematical Doklady, 148:768–770, 1963.

    Google Scholar 

  48. G. Mints. Gentzen-type systems and resolution rules. part I. propositional logic. In P. Martin-Löf and G. Mints, editors, COLOG-88, volume 417 of Lecture Notes in Computer Science, pages 198–231. Springer Verlag, 1990.

    Google Scholar 

  49. M. Moser, C. Lynch, and J. Steinbach. Model elimination with basic ordered paramodulation. Technical Report AR-95-11, Fakultät für Informatik, Technische Universität München, München, 1995.

    Google Scholar 

  50. R. Nieuwenhuis and A. Rubio. Basic superposition is complete. In ESOP'92, volume 582 of Lecture Notes in Computer Science, pages 371–389. Springer Verlag, 1992.

    Google Scholar 

  51. R. Nieuwenhuis. Simple LPO constraint solving methods. Information Processing Letters, 47:65–69, 1993.

    Article  Google Scholar 

  52. R. Nieuwenhuis and A. Rubio. Theorem proving with ordering and equality constrained clauses. Journal of Symbolic Computations, 19:321–351, 1995.

    Article  Google Scholar 

  53. S.A. Norgela. On the size of derivations under minus-normalization (in Russian). In V.A. Smirnov, editor, The Theory of Logical Inference. Institute of Philosophy, Moscow, 1974.

    Google Scholar 

  54. U. Petermann. A complete connection calculus with rigid E-unification. In JELIA '94, volume 838 of Lecture Notes in Computer Science, pages 152–166, 1994.

    Google Scholar 

  55. D.A. Plaisted. Special cases and substitutes for rigid E-unification. Technical Report MPI-I-95-2-010, Max-Planck-Institut für Informatik, November 1995.

    Google Scholar 

  56. D. Prawitz. An improved proof procedure. In J. Siekmann and G. Wrightson, editors, Automation of Reasoning. Classical Papers on Computational Logic, volume 1, pages 162–201. Springer Verlag, 1983. Originally appeared in 1960.

    Google Scholar 

  57. G. Robinson and L.T. Wos. Paramodulation and theorem-proving in first order theories with equality. In Meltzer and Michie, editors, Machine Intelligence, volume 4, pages 135–150. Edinburgh University Press, Edinburgh, 1969.

    Google Scholar 

  58. J. Schumann. Tableau-based theorem provers: Systems and implementations. Journal of Automated Reasoning, 13(3):409–421, 1994.

    Google Scholar 

  59. R. Shostak. An algorithm for reasoning about equality. Communications of the ACM, 21:583–585, July 1978.

    Article  Google Scholar 

  60. R.M. Smullyan. First-Order Logic. Springer Verlag, 1968.

    Google Scholar 

  61. A. Voronkov. On proof search in intuitionistic logic with equality, or back to simultaneous rigid E-unification. To appear in CADE'96, 15 pages, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computing Science Department, Uppsala University, Box 311, S-751 05, Uppsala, Sweden

    Anatoli Degtyarev & Andrei Voronkov

Authors
  1. Anatoli Degtyarev
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrei Voronkov
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

José Jülio Alferes Luís Moniz Pereira Ewa Orlowska

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Degtyarev, A., Voronkov, A. (1996). What you always wanted to know about rigid E-unification. In: Alferes, J.J., Pereira, L.M., Orlowska, E. (eds) Logics in Artificial Intelligence. JELIA 1996. Lecture Notes in Computer Science, vol 1126. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61630-6_4

Download citation

  • DOI: https://doi.org/10.1007/3-540-61630-6_4

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61630-6

  • Online ISBN: 978-3-540-70643-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation