Skip to main content
SpringerLink
Log in

Simplification and Backjumping in Modal Tableau

  • Conference paper
  • First Online:
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 1998)

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

Abstract

This paper is concerned with various schemes for enhancing the performance of modal tableau procedures. It discusses techniques and strategies for dealing with the nondeterminism in tableau calculi, as well as simplification and backjumping. Benchmark results obtained with randomly generated modal formulae show the effect of combinations of different schemes.

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 74.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever

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. F. Baader and B. Hollunder. A terminological knowledge representation system with complete inference algorithms. In H. Boley and M. M. Richter, editors, Proc. of the Intern. Workshop on Processing Declarative Knowledge (PDK’ 91), LNAI 567, pages 67–86. Springer, 1991.

    Google Scholar 

  2. L. Catach. Tableaux: A general theorem prover for modal logics. Journal of Automated Reasoning, 7(4):489–510, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  3. M. D’Agostino. Are tableaux an improvement on truth-tables? Journal of Logic, Language, and Information, 1:235–252, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  4. M. D’Agostino and M. Mondadori. The taming of the cut. Classical refutations with analytic cut. Journal of Logic and Computation, 4(3):285–319, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  5. R. Dechter. Enhancement schemes for constraint processing: Backjumping, learning, and cutset decomposition. Artifical Intelligence, 41(3):273–312, 1989/90.

    Article  MathSciNet  Google Scholar 

  6. M. Fitting. Proof Methods for Modal and Intuitionistic Logics, volume 169 of Synthese Library, Studies in Epistemology, Logic, Methodology, and Philosophy of Science. D. Reidel Publishing Company, 1983.

    Google Scholar 

  7. F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedures: Case study of modal K. In M. A. McRobbie and J. K. Slaney, editors, Proc. of the 13th Intern. Conf. on Automated Deduction (CADE-13), LNAI 1104, pages 583–597. Springer, 1996.

    Google Scholar 

  8. R. Goré. Tableau methods for modal and temporal logics. Technical Report TR-ARP-15-95, Automated Reasoning Project, Australian National University, Canberra, Australia, November 1995.

    Google Scholar 

  9. A. Heuerding, G. Jäger, S. Schwendimann, and M. Seyfried. The Logics Workbench LWB: A snapshot. Euromath Bulletin, 2(1):177–186, 1996.

    Google Scholar 

  10. I. Horrocks. Optimisation techniques for expressive description logics. Technical Report UMCS-97-2-1, Department of Computer Science, University of Manchester, Manchester, UK, February 1997.

    Google Scholar 

  11. U. Hustadt and R. A. Schmidt. On evaluating decision procedures for modal logic. Research report MPI-I-97-2-003, Max-Planck-Institut für Informatik, Saarbrücken, Germany, February 1997.

    Google Scholar 

  12. U. Hustadt and R. A. Schmidt. On evaluating decision procedures for modal logic. In M. E. Pollack, editor, Proc. of the Fifteenth Intern. Joint Conf. on Artificial Intelligence (IJCAI’97), pages 202–207. Morgan Kaufmann, 1997.

    Google Scholar 

  13. A. K. Mackworth. Constraint satisfaction. In S. C. Shapiro, editor, Encyclopedia of Artificial Intelligence, pages 205–211. John Wiley & Sons, 1987.

    Google Scholar 

  14. F. Massacci. Simplification with renaming: A general proof technique for tableau and sequent-based provers. Technical Report 424, Computer Laboratory, University of Cambridge, Cambridge, UK, May 1997.

    Google Scholar 

  15. J. Pitt and J. Cunningham. Theorem proving and model building with the calculus ke. Journal of the IGPL, 4(1):129–150, February 1996.

    Article  MATH  MathSciNet  Google Scholar 

  16. R. M. Smullyan. First-order logic. Springer, New York, 1968.

    MATH  Google Scholar 

  17. R. M. Stallman and G. J. Sussman. Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis. Artifical Intelligence, 9:135–196, 1977.

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing, Manchester Metropolitan University, Chester Street, Manchester, M1 5GD, UK

    Ullrich Hustadt & Renate A. Schmidt

Authors
  1. Ullrich Hustadt
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Renate A. Schmidt
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Philosophy, Tilburg University, P.O. Box 90153, 5000 LE, Tilburg, The Netherlands

    Harrie de Swart

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hustadt, U., Schmidt, R.A. (1998). Simplification and Backjumping in Modal Tableau. In: de Swart, H. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1998. Lecture Notes in Computer Science(), vol 1397. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-69778-0_22

Download citation

  • DOI: https://doi.org/10.1007/3-540-69778-0_22

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64406-4

  • Online ISBN: 978-3-540-69778-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation