CADE, 1998 Bernhard Beckert and Rajeev Gore System Description: leanK 2.0 leanK is a "lean", i.e., extremely compact, Prolog implementation of a free variable tableau calculus for propositional modal logics. leanK 2.0 includes additional search space restrictions and fairness strategies, giving a decision procedure for the logics K, KT, and S4.