TABLEAUX '98
Bernhard Beckert and Rajeev Gore
leanK 2.0 implements an extension of the "Free Variable Tableaux for
Propositional Modal Logics" reported by us at last years TABLEAUX
conference. It performs depth first search and is based upon the
original leanTAP prover of Beckert and Posegga. Formulae annotated
with labels containing variables capture the universal and existential
nature of the box and diamond modalities, respectively, with different
variable bindings closing different branches. Prolog's built-in clause
indexing scheme, unification facilities and built-in backtracking are
used extensively.
In its new version, leanK's calculus includes additional methods for
restriction the search space, which turn it into a decision procedure
for the logics K, KT, and S4.