We present a cut-free tableau calculus with histories and variables for the EXPTIME-complete multi-modal logic of common knowledge. 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||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Free-Variable Tableaux for Propositional Modal Logics.Bernhard Beckert & Rajeev GorÉ - 2001 - Studia Logica 69 (1):59-96.
Are Tableaux an Improvement on Truth-Tables?Marcello D'Agostino - 1992 - Journal of Logic, Language and Information 1 (3):235-252.
Cut-Free Tableau Calculi for Some Propositional Normal Modal Logics.Martin Amerbauer - 1996 - Studia Logica 57 (2-3):359 - 372.
Cut-Elimination and Proof-Search for Bi-Intuitionistic Logic Using Nested Sequents.Rajeev Gore, Linda Postniece & Alwen Tiu - unknown
Combining Derivations and Refutations for Cut-Free Completeness in Bi-Intuitionistic Logic.Linda Postniece - unknown
Added to index2009-01-28
Total downloads171 ( #26,938 of 2,172,772 )
Recent downloads (6 months)1 ( #325,028 of 2,172,772 )
How can I increase my downloads?