Simplification and Backjumping in Modal Tableau
- 231 Downloads
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.
KeywordsPropositional Variable Elimination Rule Modal Formula Standard Tableau Negation Normal Form
Unable to display preview. Download preview PDF.
- 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
- 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