Skip to main content
SpringerLink
Log in

Incremental theory reasoning methods for semantic tableaux

  • Contributed Papers
  • Conference paper
  • First Online:
Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX 1996)

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

Abstract

Theory reasoning is an important technique for increasing the efficiency of automated deduction systems. In this paper we present incremental theory reasoning, a method that improves the interaction between the foreground reasoner and the background (theory) reasoner and, thus, the efficiency of the combined system. The use of incremental theory reasoning in free variable semantic tableaux and the cost reduction that can be achieved are discussed; as an example, completion-based equality reasoning is presented, including experimental data obtained using an implementation.

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. M. Baaz and C. G. Fermüller. Non-elementary speedups between different versions of tableaux. In Proceedings, 4th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, St. Goar, LNCS 918, pages 217–230. Springer, 1995.

    Google Scholar 

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

  3. P. Baumgartner. Linear and unit-resulting refutations for Horn theories. Journal of Automated Reasoning, 1996. To appear.

    Google Scholar 

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

    Google Scholar 

  5. B. Beckert. Adding equality to semantic tableaux. In K. Broda, M. D'Agostino, R. Gore, R. Johnson, and S. Reeves, editors, Proceedings, 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Abingdon, pages 29–41, Imperial College, London, TR-94/5, 1994.

    Google Scholar 

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

  7. B. Beckert, S. Gerberding, R. Hähnle, and W. Kernig. The tableau-based theorem prover 3 T AP for multiple-valued logics. In Proceedings, 11th International Conference on Automated Deduction (CADE), Saratoga Springs, NY, LNCS 607, pages 758–760. Springer, 1992.

    Google Scholar 

  8. B. Beckert, R. Hähnle, K. Geiß, P. Oel, C. Pape, and M. Sulzmann. The manyvalued tableau-based theorem prover 3T Ap, version 4.0. Interner Bericht 3/96, Universität Karlsruhe, Fakultät für Informatik, 1996.

    Google Scholar 

  9. B. Beckert, R. Hähnle, and P. H. Schmitt. The even more liberalized δ-rule in free variable semantic tableaux. In G. Gottlob, A. Leitsch, and D. Mundici, editors, Proceedings, 3rd Kurt Gödel Colloquium (KGC), Brno, Czech Republic, LNCS 713, pages 108–119. Springer, 1993.

    Google Scholar 

  10. W. Bibel. Automated Theorem Proving. Vieweg, Braunschweig, second revised edition, 1987.

    Google Scholar 

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

  12. A. Degtyarev and A. Voronkov. Simultaneous rigid E-unification is undecidable. UPMAIL Technical Report 105, Uppsala University, May 1995. Presented at: Annual Conference of the European Association for Computer Science Logic (CSL'95), Paderborn.

    Google Scholar 

  13. M. C. Fitting. First-Order Logic and Automated Theorem Proving. Springer, 1990.

    Google Scholar 

  14. 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, Apr. 1992.

    Google Scholar 

  15. R. Hähnle and P. H. Schmitt. The liberalized δ-rule in free variable semantic tableaux. Journal of Automated Reasoning, 13(2):211–222, 1994.

    Google Scholar 

  16. D. E. Knuth and P. B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebras, pages 263–297. Pergamon Press, Oxford, 1970.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  19. W. Nutt, P. Réty, and G. Smolka. Basic narrowing revisited. Journal of Symbolic Computation, 7(3/4):295–318, 1989.

    Google Scholar 

  20. F. J. Pelletier. Seventy-five problems for testing automatic theorem provers. Journal of Automated Reasoning, 2:191–216, 1986.

    Google Scholar 

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

  22. R. Smullyan. First-Order Logic. Springer, 1968.

    Google Scholar 

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

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute for Logic, Complexity and Deduction Systems, University of Karlsruhe, Am Fasanengarten 5, 76128, Karlsruhe, Germany

    Bernhard Beckert & Christian Pape

Authors
  1. Bernhard Beckert
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christian Pape
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

P. Miglioli U. Moscato D. Mundici M. Ornaghi

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Beckert, B., Pape, C. (1996). Incremental theory reasoning methods for semantic tableaux. In: Miglioli, P., Moscato, U., Mundici, D., Ornaghi, M. (eds) Theorem Proving with Analytic Tableaux and Related Methods. TABLEAUX 1996. Lecture Notes in Computer Science, vol 1071. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61208-4_7

Download citation

  • DOI: https://doi.org/10.1007/3-540-61208-4_7

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61208-7

  • Online ISBN: 978-3-540-68368-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation