Simplification and Backjumping in Modal Tableau

  • Ullrich Hustadt
  • Renate A. Schmidt
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1397)


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.


Propositional Variable Elimination Rule Modal Formula Standard Tableau Negation Normal Form 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 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. 2.
    L. Catach. Tableaux: A general theorem prover for modal logics. Journal of Automated Reasoning, 7(4):489–510, 1991.zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    M. D’Agostino. Are tableaux an improvement on truth-tables? Journal of Logic, Language, and Information, 1:235–252, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  4. 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.zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    R. Dechter. Enhancement schemes for constraint processing: Backjumping, learning, and cutset decomposition. Artifical Intelligence, 41(3):273–312, 1989/90.CrossRefMathSciNetGoogle Scholar
  6. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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.zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    R. M. Smullyan. First-order logic. Springer, New York, 1968.zbMATHGoogle Scholar
  17. 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.zbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Ullrich Hustadt
    • 1
  • Renate A. Schmidt
    • 1
  1. 1.Department of ComputingManchester Metropolitan UniversityManchesterUK

Personalised recommendations