The Tableau WorkBench (TWB)

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.