Skip to main content
SpringerLink
Log in

Equality and Other Theories

  • Chapter
Handbook of Tableau Methods

Abstract

Theory reasoning is an important technique for increasing the efficiency of automated deduction systems. The knowledge from a given domain (or theory) is made use of by applying efficient methods for reasoning in that domain. The general purpose foreground reasoner calls a special purpose background reasoner to handle problems from a certain theory.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 169.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 219.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 219.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P. B. Andrews. Theorem proving through general matings. Journal of the ACM, 28: 193–214, 1981.

    Article  Google Scholar 

  2. L. Bachmair, H. Ganzinger and A. Voronkov. Elimination of equality via transformation with ordering constraints. Technical Report MPI–I–97–2–012, MPI für Informatik, Saarbrücken, 1997.

    Google Scholar 

  3. P. Baumgartner. A model elimination calculus with built-in theories. In H.-J. Ohlbach, editor, Proceedings, German Workshop on Artificial Intelligence (GWAI), LNCS 671, pages 30–42. Springer, 1992.

    Google Scholar 

  4. P. Baumgartner. Linear and unit-resulting refutations fer Horn theories. Journal of Automated Reasoning, 16 (3): 241–319, 1996.

    Article  Google Scholar 

  5. P. Baumgartner. Theory Reasoning in Connection Calculi. LNCS. Springer, 1998. To appear.

    Google Scholar 

  6. P. Baumgartner, U. Furbach, and U. Petermann. A unified approach to theory reasoning. Forschungsbericht 15/92, University of Koblenz, 1992.

    Google Scholar 

  7. P. Baumgartner and U. Petermann. Theory reasoning. In W. Bibel and P. H. Schmitt, editors, Automated Deduction — A Basis for Applications, volume I. Kluwer, 1998.

    Google Scholar 

  8. G. Becher and U. Petermann. Rigid unification by completion and rigid paramodulation. In B. Nebel and L. Dreschler-Fischer, editors, Proceedings, 18th German Annual Conference on Artificial Intelligence (KI-94), Saarbrücken, Germany, LNCS 861, pages 319–330. Springer, 1994.

    Google Scholar 

  9. B. Beckert. A completion-based method for mixed universal and rigid E-unification. In A. Bundy, editor, Proceedings, 12th International Conference on Automated Deduction (CADE), Nancy, France, LNCS 814, pages 678–692. Springer, 1994.

    Google Scholar 

  10. B. Beckert. Semantic tableaux with equality. Journal of Logic and Computation, 7 (1): 39–58, 1997.

    Article  Google Scholar 

  11. B Beckert. Rigid E-unification. In W. Bibel and P. H. Schmitt, editors, Automated Deduction —A Basis for Applications, volume I. Kluwer, 1998.

    Google Scholar 

  12. B. Beckert and R. Hähnle. An improved method for adding equality to free variable semantic tableaux. In D. Kapur, editor, Proceedings, 11th International Conference on Automated Deduction (CADE), Saratoga Springs, NY, USA, LNCS 607, pages 507–521. Springer, 1992.

    Google Scholar 

  13. B. Beckert and R. Hähnle. Analytic tableaux. In W. Bibel and P. H. Schmitt, editors, Automated Deduction — A Basis for Applications, volume I. Kluwer, 1998.

    Google Scholar 

  14. B. Becken, R. Hähnle, P. Oel and M. Sulzmann. The tableau-based theorem prover 3IxlP, version 4.0. In Proceedings, 13th International Conference on Automated Deduction (CADE), New Brunswick, NJ, USA, LNCS 1104, pages 303–307. Springer, 1996.

    Google Scholar 

  15. B. Beckett and C. Pape. Incremental theory reasoning methods for semantic tableaux. In P. Miglioli, U. Moscato, D. Mundici, and M. Omaghi, editors, Proceedings, 5th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Palermo, Italy, LNCS 1071, pages 93–109. Springer, 1996.

    Google Scholar 

  16. W. Bibel. Automated Theorem Proving. Vieweg, Braunschweig, second edition, 1987. First edition published in 1982.

    Google Scholar 

  17. D. Brand. Proving theorems with the modification method. SIAM Journal on Computing, 4 (4): 412–430, 1975.

    Article  Google Scholar 

  18. R. J. Browne. Ground term rewriting in semantic tableaux systems for first-order logic with equality. Technical Report UMIACS-TR-88–44, College Park, MD, 1988.

    Google Scholar 

  19. H. Bürckert. A resolution principle for clauses with constraints. In Proceedings, 10th International Conference on Automated Deduction (CADE), LNCS 449, pages 178–192. Springer, 1990.

    Google Scholar 

  20. D. Cantone, A. Ferro and E. Omodeo. Computable Set Theory, volume 6 of International Series of Motwgraphs on Computer Science. Oxford University Press, 1989.

    Google Scholar 

  21. E. de Kogel. Rigid E-unification simplified. In Proceedings, 4th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, St. Goar, LNCS 918, pages 17–30. Springer, 1995.

    Google Scholar 

  22. A. Degtyarev and A. Voronkov. Equality elimination for the tableau method. In J. Calmet and C. Limongelli, editors, Proceedings, International Symposium on Design and Implementation of Symbolic Computation Systems (DISCO), Karlsruhe, Germany, LNCS 1128, pages 46–60, 1996.

    Google Scholar 

  23. A. Degtyarev and A. Voronkov. Simultaneous rigid E-unification is undecidable. In H. Kleine Büning, editor, Proceedings, Annual Conference of the European Association for Computer Science Logic (CSL’95), LNCS 1092, pages 178–190. Springer, 1996.

    Google Scholar 

  24. A. Degtyarev and A. Voronkov. What you always wanted to know about rigid E-unification. Journal of Automated Reasoning, 20 (1): 47–80, 1998.

    Article  Google Scholar 

  25. V. J. Digricoli and M. C. Harrison. Equality-based binary resolution. Journal of the ACM, 33 (2): 253–289, April 1986.

    Article  Google Scholar 

  26. M. C. Fitting. First-Order Logic and Automated Theorem Proving. Springer, 1996. First edition, 1990.

    Google Scholar 

  27. U. Furbach. Theory reasoning in first order calculi. In K. v. Luck and H. Marburger, editors, Proceedings, Third Workshop on Information Systems and Artificial Intelligence, Hamburg, Germany, LNCS 777, pages 139–156. Springer, 1994.

    Google Scholar 

  28. J. H. Gallier, P. Narendran, D. Plaisted and W Snyder. Rigid E-unification is NP-complete. In Procceedings, Symposium on Logic in Computer Science (LICS) IEEE Press, 1988.

    Google Scholar 

  29. J. H. Gallier, P. Narendran, D. Plaisted, and W. Snyder. Rigid E-unification: NP-completeness and application to equational matings. Information and Computation, pages 129–195, 1990.

    Google Scholar 

  30. J. H. Gallier, P. Narendran, S. Raatz, and W. Snyder. Theorem proving using equational matings and rigid E-unification. Journal of the ACM, 39 (2): 377–429, April 1992.

    Article  Google Scholar 

  31. J. H. Gallier, S. Raatz, and W. Snyder. Theorem proving using rigid E-unification, equational matings. In Proceedings, Symposium on Logic in Computer Science (LICS), Ithaka, NY, USA IEEE Press, 1987.

    Google Scholar 

  32. J. H. Gallier and W. Snyder. Designing unification procedures using transformations: A survey. Bulletin of the EATCS, 40: 273–326, 1990.

    Google Scholar 

  33. G. Grieser. An implementation of rigid E-unification using completion and rigid paramodulation. Forschungsbericht FITL-96–4, FIT Leipzig e.V., 1996.

    Google Scholar 

  34. Y. Gurevich and M. Veanes. Some undecidable problems related to the Herbrand theorem. UPMAIL Technical Report 138, Uppsala University, 1997.

    Google Scholar 

  35. R. C. Jeffrey. Formal Logic. Its Scope and Limits. McGraw-Hill, New York, 1967.

    Google Scholar 

  36. J.-P. Jouannaud and C. Kirchner. Solving equations in abstract algebras: A rule-based survey of unification. In J. Lassez and G. Plotkin, editors, Computational Logic — Essays in Honor of Alan Robinson, pages 257–321. MIT Press, 1991.

    Google Scholar 

  37. S. Kanger. A simplified proof method for elementary logic. In P. Braffort and D. Hirschberg, editors, Computer Programming and Formal Systems,pages 87–94. North Holland, 1963. Reprint as pages 364–371, Siekmann, J., and Wrightson, G. (eds.), Automation of Reasoning. Classical Papers on Computational Logic,vol. 1. Springer, 1983.

    Google Scholar 

  38. D. Kozen. Positive first-order logic is NP-complete. IBM Journal of Research and Development, 25 (4): 327–332, 1981.

    Article  Google Scholar 

  39. Z. Lis. Wynikanie semantyczne a wynikanie formalise. Studia Logica,10:39–60, 1960. In Polish with English summary.

    Google Scholar 

  40. D. W. Loveland. A simplified format for the model elimination procedure. Journal of the ACM, 16 (3): 233–248, 1969.

    Article  Google Scholar 

  41. N. V. Murray and E. Rosenthal. Inference with path resolution and semantic graphs. Journal of the ACM, 34 (2): 225–254, April 1987.

    Article  Google Scholar 

  42. N. V. Murray and E. Rosenthal. Theory links: Applications to automated theorem proving. Journal of Symbolic Computation, 4: 173–190, 1987.

    Article  Google Scholar 

  43. G. Nelson and D. C. Oppen. Fast decision procedures based on congruence closure. Journal of the ACM, 27 (2): 356–364, April 1980.

    Article  Google Scholar 

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

    Article  Google Scholar 

  45. U. Petermann. How to build-in an open theory into connection calculi. Journal on Computer and Artificial Intelligence, 11 (2): 105–142, 1992.

    Google Scholar 

  46. U. Petermann. Completeness of the pool calculus with an open built-in theory. In G. Gottlob, A. Leitsch, and D. Mundici, editors, Proceedings, 3rd Kurt Gödel Colloquium (KGC), Brno, Czech Republic, LNCS 713, pages 264–277. Springer, 1993.

    Google Scholar 

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

    Google Scholar 

  48. A. Policriti and J. T. Schwartz. T-theorem proving I. Journal of Symbolic Computation, 20: 315–342, 1995.

    Article  Google Scholar 

  49. R. J. Popplestone. Beth-tree methods in automatic theorem proving. In N. Collins and D. Michie, editors, Machine Intelligence, volume 1, pages 31–46. Oliver and Boyd, 1967.

    Google Scholar 

  50. S. V. Reeves. Adding equality to semantic tableau. Journal of Automated Reasoning, 3: 225–246, 1987.

    Article  Google Scholar 

  51. J. A. Robinson and L. Wos. Paramodulation and theorem proving in first order theories with equality. In B. Meltzer and D. Michie, editors, Machine Intelligence. Edinburgh University Press, 1969.

    Google Scholar 

  52. R. E. Shostak. An algorithm for reasoning about equality. Communications of the ACM, 21 (7): 583–585, 1978.

    Article  Google Scholar 

  53. J. H. Siekmann. Universal unification. Journal of Symbolic Computation,7(3/4):207–274, 1989. Earlier version in Proceedings, 7th International Conference on Automated Deduction (CADE), Napa, FL. USA,LNCS 170, Springer, 1984.

    Google Scholar 

  54. R. M. Smullyan. First-Order Logic. Dover Publications, New York, second corrected edition, 1995. First published in 1968 by Springer.

    Google Scholar 

  55. W. Snyder. A Proof Theory for General Unification. Birkhäuser, Boston, 1991.

    Google Scholar 

  56. M. E. Stickel. Automated deduction by theory resolution. Journal of Automated Reasoning, 1: 333–355, 1985.

    Article  Google Scholar 

  57. M. Veanes. On Simultaneous Rigid E-Unification. PhD Thesis, Uppsala University, Sweden, 1997.

    Google Scholar 

  58. P. Voda and J. Komara. On Herbrand skeletons. Technical Report mff-ii-02–1995, Institute of Informatics, Comenius University, Bratislava, Slovakia, 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universität Karlsruhe, Germany

    Bernhard Beckert

Authors
  1. Bernhard Beckert
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Università di Ferrara, Ferrara, Italy

    Marcello D’Agostino

  2. King’s College, London, UK

    Dov M. Gabbay

  3. Universität Karlsruhe, Germany

    Reiner Hähnle

  4. Research Centre, Deutsche Telekom AG, Darmstadt, Germany

    Joachim Posegga

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer Science+Business Media Dordrecht

About this chapter

Cite this chapter

Beckert, B. (1999). Equality and Other Theories. In: D’Agostino, M., Gabbay, D.M., Hähnle, R., Posegga, J. (eds) Handbook of Tableau Methods. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-1754-0_4

Download citation

  • DOI: https://doi.org/10.1007/978-94-017-1754-0_4

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-90-481-5184-4

  • Online ISBN: 978-94-017-1754-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation