Cut-free single-pass tableaux for the logic of common knowledge
| Abstract | We present a cut-free tableau calculus with histories and variables for the EXPTIME-complete multi-modal logic of common knowledge (LCK). Our calculus constructs the tableau using only one pass, so proof-search for testing theoremhood of ϕ does not exhibit the worst-case EXPTIME-behaviour for all ϕ as in two-pass methods. Our calculus also does not contain a “finitized ω-rule” so that it detects cyclic branches as soon as they arise rather than by worst-case exponential branching with respect to the size of ϕ. Moreover, by retaining the rooted-tree form from traditional tableaux, our calculus becomes amenable to the vast array of optimisation techniques which have proved essential for “practical” automated reasoning in very expressive description logics. Our calculus forms the basis for developing a uniform framework for the family of all fix-point logics of common knowledge. However, there is still no “free lunch” as, in the worst case, our method exhibits 2EXPTIME-behaviour. A prototype implementation can be found at twb.rsise.anu.edu.au which allows users to test formulae via a simple graphical interface. | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,701 |
| External links |
  Try with proxy. |
| Through your library | Only published papers are available at libraries |
Similar books and articlesBernhard Beckert & Rajeev GorÉ (2001). Free-Variable Tableaux for Propositional Modal Logics. Studia Logica 69 (1):59-96.
Marcello D'Agostino (1992). Are Tableaux an Improvement on Truth-Tables? Journal of Logic, Language and Information 1 (3):235-252.
Brian Hill & Francesca Poggiolesi (2010). A Contraction-Free and Cut-Free Sequent Calculus for Propositional Dynamic Logic. Studia Logica 94 (1).
Martin Amerbauer (1996). Cut-Free Tableau Calculi for Some Propositional Normal Modal Logics. Studia Logica 57 (2-3):359 - 372.
Katalin Bimbó (2007). $LE^{T}{Rightarrow}$ , $LR^{Circ}{Wedgesim}$ , LK and Cutfree Proofs. Journal of Philosophical Logic 36 (5):557 - 570.
Carlo Cellucci (2000). Analytic Cut Trees. Logic Journal of the IGPL 8:733-750.
Analytics
Monthly downloads |
Added to index2009-01-28Total downloads6 ( #145,673 of 549,128 )Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
