Graduate studies at Western
Journal of Logic, Language and Information 14 (3):289-329 (2005)
|Abstract||We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF2, which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. The translation is theoretically interesting because it translates modal logics with certain frame conditions into first-order logic, without explicitly expressing the frame conditions. It is practically relevant because it makes it possible to use a decision procedure for the guarded fragment in order to decide regular grammar logics with converse. The class of regular grammar logics includes numerous logics from various application domains. A consequence of the translation is that the general satisfiability problem for every regular grammar logics with converse is in EXPTIME. This extends a previous result of the first author for grammar logics without converse. Other logics that can be translated into GF2 include nominal tense logics and intuitionistic logic. In our view, the results in this paper show that the natural first-order fragment corresponding to regular grammar logics is simply GF2 without extra machinery such as fixed-point operators.|
|Keywords||modal and temporal logics relational translation guarded fragment|
|Categories||categorize this paper)|
|Through your library||Configure|
Similar books and articles
Alexander S. Karpenko (2000). The Classification of Propositional Calculi. Studia Logica 66 (2):253-271.
Kosta Došen (1992). Modal Translations in Substructural Logics. Journal of Philosophical Logic 21 (3):283 - 336.
Heinrich Wansing (1999). Predicate Logics on Display. Studia Logica 62 (1):49-75.
Minghui Ma (2010). Toward Model-Theoretic Modal Logics. Frontiers of Philosophy in China 5 (2):294-311.
Jacek K. Kabziński (1982). Basic Properties of the Equivalence. Studia Logica 41 (1):17 - 40.
Kazimierz Świrydowicz (1990). On Regular Modal Logics with Axiom □ ⊤ → □□ ⊤. Studia Logica 49 (2):171 - 174.
Roman Kontchakov, Agi Kurucz & Michael Zakharyaschev (2005). Undecidability of First-Order Intuitionistic and Modal Logics with Two Variables. Bulletin of Symbolic Logic 11 (3):428-438.
Linh Anh Nguyen & Andrzej Szałas (2011). ExpTime Tableau Decision Procedures for Regular Grammar Logics with Converse. Studia Logica 98 (3):387-428.
Added to index2009-01-28
Total downloads2 ( #246,325 of 739,315 )
Recent downloads (6 months)0
How can I increase my downloads?