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.