paper submitted to AGENTS, LOGIC AND THEOREM PROVING workshop at TABLEAUX 2007
Abstract:
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 j does not exhibit the worst-case EXPTIME-behaviour for all j
as in two-pass methods. Our calculus also does not contain a “finitized w-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 j. 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 via the web.
Attachment | Size |
---|---|
abate-gore-widmann-lck-tab07.pdf | 73.23 KB |
abate-gore-widmann-lck-tab07-FULL.pdf | 240.13 KB |