Abstract
This paper ties together two distinct strands in automated reasoning: the tableau- and the automata-based approach. It shows that the inverse tableau method can be viewed as an implementation of the automata approach. This is of interest to automated deduction because Voronkov recently showed that the inverse method yields a viable decision procedure for the modal logic K.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
C. Areces, R. Gennari, J. Heguiabehere, and M. de Rijke. Tree-based heuristics in modal theorem proving. In W. Horn, editor, Proc. of ECAI2000, Berlin, Germany, 2000. IOS Press Amsterdam.
F. Baader and U. Sattler. An overview of tableau algorithms for description logics. Studia Logica, 2001. To appear.
F. Baader and S. Tobies. The inverse method implements the automata approach for modal satisfiability. LTCS-Report 01-03, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2001. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. Cambridge University Press, 2001. Publishing date May 2001, preliminary version available online from http://www.mlbook.org/.
C. Courcoubetis, M. Y. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. In E. M. Clarke and R. P. Kurshan, editors, Proc. of Computer-Aided Verification (CAV’ 90), volume 531 of LNCS, pages 233–242. Springer Verlag, 1991.
F. M. Donini and F. Massacci. EXPTIME tableaux for ALC. Artificial Intelligence, 124(1):87–138, 2000.
W. F. Dowling and J. H. Gallier. Linear-time algorithms for testing the satisfiability of propositional horn formulae. Journal of Logic Programming, 1(3):267-28, 1984.
R. Dyckhoff, editor. Proc. of TABLEAUX 2000, number 1847 in LNAI, St Andrews, Scotland, UK, 2000. Springer Verlag.
R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper. Simple on-the-fly Automatic verification of linear temporal logic. In Proc. of the 15th International Symposium on Protocol Specification, Testing, and Verification, pages 3–18, Warsaw, Poland, 1995. Chapman & Hall.
R. Goré. Tableau methods for modal and temporal logics. In M. D’Agostino, D. M. Gabbay, R. Hähnle, and J. Posegga, editors, Handbook of Tableau Methods. Kluwer, Dordrecht, 1998.
I. Horrocks. Benchmark analysis with FaCT. In Dyckhoff[8], pages 62–66.
U. Hustadt and R. A. Schmidt. MSPASS: Modal reasoning by translation and first-order resolution. In Dyckhoff [8], pages 67–71.
R. E. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM Journal on Computing, 6(3):467–480, 1977.
C. Lutz and U. Sattler. The complexity of reasoning with boolean modal logic. In Wolter F., H. Wansing, M. de Rijke, and M. Zakharyaschev, editors, Preliminary Proc. of AiML2000, Leipzig, Germany, 2000.
R. A. Schmidt. Resolution is a decision procedure for many propositional modal logics. In M. Kracht, M. de Rijke, H. Wansing, and M. Zakharyaschev, editors, Advances in Modal Logic, Volume 1, volume 87 of Lecture Notes, pages 189–208. CSLI Publications, Stanford, 1998.
E. Spaan. Complexity of Modal Logics. PhD thesis, Univ. van Amsterdam, 1993.
M. Y. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. Journal of Computer and System Sciences, 32:183–221, 1986.
M. Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115:1–37, 1994.
A. Voronkov. How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi. ACM Transactions on Computational Logic, 1(4):35pp, 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baader, F., Tobies, S. (2001). The Inverse Method Implements the Automata Approach for Modal Satisfiability. In: Goré, R., Leitsch, A., Nipkow, T. (eds) Automated Reasoning. IJCAR 2001. Lecture Notes in Computer Science, vol 2083. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45744-5_8
Download citation
DOI: https://doi.org/10.1007/3-540-45744-5_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42254-9
Online ISBN: 978-3-540-45744-2
eBook Packages: Springer Book Archive