A tableau calculus with automaton-labelled formulae for regular grammar logics
| Abstract | We present a sound and complete tableau calculus for the class of regular grammar logics. Our tableau rules use a special feature called automaton-labelled formulae, which are similar to formulae of automaton propositional dynamic logic. Our calculus is cut-free and has the analytic superformula property so it gives a decision procedure. We show that the known EXPTIME upper bound for regular grammar logics can be obtained using our tableau calculus. We also give an effective Craig interpolation lemma for regular grammar logics using our calculus. | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | No categories specified (fix it) | |||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,672 |
| External links |
  Try with proxy. |
| Through your library | Only published papers are available at libraries |
Similar books and articlesA. V. Kuznetsov & A. Yu Muravitsky (1986). On Superintuitionistic Logics as Fragments of Proof Logic Extensions. Studia Logica 45 (1):77 - 99.
Franz Baader & Ulrike Sattler (2001). An Overview of Tableau Algorithms for Description Logics. Studia Logica 69 (1):5-40.
Riccardo Rosati (2001). A Sound and Complete Tableau Calculus for Reasoning About Only Knowing and Knowing at Most. Studia Logica 69 (1):171-191.
P. J. Martín & A. Gavilanes (2002). Simultaneous Rigid Sorted Unification for Tableaux. Studia Logica 72 (1):31-59.
Linh Anh Nguyen (2001). Analytic Tableau Systems and Interpolation for the Modal Logics KB, KDB, K5, KD. Studia Logica 69 (1):41-57.
Martin Amerbauer (1996). Cut-Free Tableau Calculi for Some Propositional Normal Modal Logics. Studia Logica 57 (2-3):359 - 372.
Stéphane Demri & Hans De Nivelle (2005). Deciding Regular Grammar Logics with Converse Through First-Order Logic. Journal of Logic, Language and Information 14 (3).
Linh Anh Nguyen & Andrzej Szałas (2011). ExpTime Tableau Decision Procedures for Regular Grammar Logics with Converse. Studia Logica 98 (3):387-428.
Analytics
Monthly downloads |
Added to index2010-05-07Total downloads2 ( #232,382 of 549,060 )Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
