Abstract
Different variants of guarded logics (a powerful generalization of modal logics) are surveyed and the recent decidability result for guarded fixed point logic (obtained in joint work with I. Walukiewicz) is explained. The exposition given here emphasizes the tree model property of guarded logics: every satisfiable sentence has a model of bounded tree width.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
H. Andréka, J. VAN Benthem, and I. Németi, Modal languages and bounded fragments of predicate logic, Journal of Philosophical Logic, 27(1998), pp. 217–274.
J. VAN Benthem, Dynamic bits and pieces, ILLC research report, University of Amsterdam, 1997.
A. Emerson and C. Jutla, The complexity of tree automata and logics of programs, in Proc. 29th IEEE Symp. on Foundations of Computer Science, 1988, pp. 328–337.
J. Flum, On the (infinite) model theory of fixed-point logics, in Models, algebras, and proofs, X. Caicedo and C. Montenegro, eds., no. 2003 in Lecture Notes in Pure and Applied Mathematics Series, Marcel Dekker, 1999, pp. 67–75.
E. Grädel, On the restraining power of guards, Journal of Symbolic Logic. To appear.
E. Grädel and I. Walukiewicz, Guarded fixed point logic, in Proc. 14th IEEE Symp. on Logic in Computer Science, 1999.
D. Kozen, Results on the propositional μ-calculus, Theoretical Computer Science, 27(1983), pp. 333–354.
M. Rabin, Decidability of second-order theories and automata on infinite trees, Transactions of the AMS, 141(1969), pp. 1–35.
B. Reed, Tree width and tangles: A new connectivity measure and some applications, in Surveys in Combinatorics, R. Bailey, ed., Cambridge University Press, 1997, pp. 87–162.
C. Stirling, Bisimulation, model checking and other games. Notes for the Mathfit instructional meeting on games and computation. Edinburgh, 1997.
M. Vardi, Why is modal logic so robustly decidable?, in Descriptive Complexity and Finite Models, N. Immerman and P. Kolaitis, eds., vol. 31 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, AMS, 1997, pp. 149–184.
—, Reasoning about the past with two-way automata, in Automata, Languages and Programming ICALP 98, vol. 1443 of Springer Lecture Notes in Computer Science, 1998, pp. 628–641.
W. Zielonka, Infinite games on finitely coloured graphs with applications to automata on infinite trees, Theoretical Computer Science, 200(1998), pp. 135–183.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Grädel, E. (1999). Decision Procedures for Guarded Logics. In: Automated Deduction — CADE-16. CADE 1999. Lecture Notes in Computer Science(), vol 1632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48660-7_3
Download citation
DOI: https://doi.org/10.1007/3-540-48660-7_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66222-8
Online ISBN: 978-3-540-48660-2
eBook Packages: Springer Book Archive