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.