Skip to main content
SpringerLink
Log in

Equality elimination for the tableau method

  • Conference paper
  • First Online:
Design and Implementation of Symbolic Computation Systems (DISCO 1996)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1128))

Abstract

We apply the equality elimination method to semantic tableaux with equality. The resulting logical system is a combination of a goal-directed tableau calculus with a basic superposition calculus. Unlike most other known methods of adding equality to semantic tableaux, equality elimination does not use simultaneous rigid E-unification or its modifications. For controlling redundancy, we can use powerful strategies of subsumption and simplification. We also make an extensive comparison with related works in the area.

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. L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basic paramodulation. Information and Computation, 121:172–192, 1995.

    Google Scholar 

  3. 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 

  4. 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 

  5. E.W. Beth. The Foundations of Mathematics. North Holland, 1959.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  8. A. Degtyarev and A. Voronkov. Automated theorem proving I and II. Cybernetics, 22(3):290–297, 1986 and 23(4):547–556, 1987.

    Google Scholar 

  9. A. Degtyarev and A. Voronkov. Equality control methods in machine theorem proving. Cybernetics, 22(3):298–307, 1986.

    Google Scholar 

  10. A. Degtyarev and A. Voronkov. Equality elimination for semantic tableaux. UP-MAIL Technical Report 90, Uppsala University, Computing Science Department, December 1994.

    Google Scholar 

  11. 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 

  12. A. Degtyarev and A. Voronkov. A new procedural interpretation of Horn clauses with equality. In Leon Sterling, editor, Proceedings of the Twelfth International Conference on Logic Programming, pages 565–579. The MIT Press, 1995.

    Google Scholar 

  13. 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.

    Google Scholar 

  14. 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 

  15. A. Degtyarev and A. Voronkov. What you always wanted to know about rigid E-unification. In Submitted to JELIA '96, page 20, 1996.

    Google Scholar 

  16. R. Demolombe. An efficient strategy for non-Horn deductive databases. In G.X. Ritter, editor, Information Processing 89, pages 325–330. Elsevier Science, 1989.

    Google Scholar 

  17. N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. Van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, chapter 6, pages 243–309. North Holland, Amsterdam, 1990.

    Google Scholar 

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

    Google Scholar 

  19. 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 

  20. 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 

  21. 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 

  22. 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 

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

    Google Scholar 

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

    Google Scholar 

  25. E.L. Lusk. Controlling redundancy in large search spaces: Argonne-style theorem proving through the years. In A. Voronkov, editor, Logic Programming and Automated Reasoning. International Conference LPAR'92., volume 624 of Lecture Notes in Artificial Intelligence, pages 96–106, St.Petersburg, Russia, July 1992.

    Google Scholar 

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

    Google Scholar 

  27. 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 

  28. S.Yu. Maslov. The generalization of the inverse method to predicate calculus with equality (in Russian). Zapiski Nauchnyh Seminarov LOMI, 20:80–96, 1971. English translation in: Journal of Soviet Mathematics 1, no. 1.

    Google Scholar 

  29. S.Yu. Maslov, G.E. Mints, and V.P. Orevkov. Mechanical proof-search and the theory of logical deduction in the USSR. In J.Siekmann and G.Wrightson, editors, Automation of Reasoning (Classical papers on Computational Logic), volume 1, pages 29–38. Springer Verlag, 1983.

    Google Scholar 

  30. 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 

  31. J. Minker, A. Rajasekar, and J. Lobo. Theory of disjunctive logic programs. In Jean-Louis Lassez and Gordon Plotkin, editors, Computational Logic. Essays in Honor of Alan Robinson., pages 613–639. The MIT Press, Cambridge, MA, 1991.

    Google Scholar 

  32. 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 

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

    Google Scholar 

  34. V.P. Orevkov. On nonlengthening rule applications for equality (in Russian). Zapiski Nauchnyh Seminarov LOMI, 16:152–156, 1969. English Translation in: Seminars in Mathematics: Steklov Math. Inst. 16, Consultants Bureau, NY-London, 1971, p.77–79.

    Google Scholar 

  35. 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 

  36. 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 

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

    Google Scholar 

  38. N. Shankar. Proof search in the intuitionistic sequent calculus. In D. Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 522–536, Saratoga Springs, NY, USA, June 1992. Springer Verlag.

    Google Scholar 

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

    Google Scholar 

  40. A. Voronkov. LISS — the logic inference search system. In Mark Stickel, editor, Proc. 10th Int. Conf. on Automated Deduction, volume 449 of Lecture Notes in Computer Science, pages 677–678, Kaiserslautern, Germany, 1990. Springer Verlag.

    Google Scholar 

  41. A. Voronkov. A proof-search method for the first order logic. In P. Martin-Löf and G. Mintz, editors, COLOG'88, volume 417 of Lecture Notes in Computer Science, pages 327–340. Springer Verlag, 1990.

    Google Scholar 

  42. A. Voronkov. Theorem proving in non-standard logics based on the inverse method. In D. Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 648–662, Saratoga Springs, NY, USA, June 1992. Springer Verlag.

    Google Scholar 

  43. H. Wang. Towards mechanical mathematics. IBM J. of Research and Development, 4:2–22, 1960.

    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

Jacques Calmet Carla Limongelli

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Degtyarev, A., Voronkov, A. (1996). Equality elimination for the tableau method. In: Calmet, J., Limongelli, C. (eds) Design and Implementation of Symbolic Computation Systems. DISCO 1996. Lecture Notes in Computer Science, vol 1128. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61697-7_4

Download citation

  • DOI: https://doi.org/10.1007/3-540-61697-7_4

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61697-9

  • Online ISBN: 978-3-540-70635-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation