U. Hustadt and R. A. Schmidt (1998): Simplification and backjumping in modal tableau

U. Hustadt and R. A. Schmidt (1998a): ``Simplification and backjumping in modal tableau.'' In H. de Swart, editor, Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'98) [Oisterwijk, The Netherlands, 5-8 May 1998], pp. 187-201. LNAI 1397, Springer.
Abstract, BibTeX, PDF (© Springer).

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.