Sciweavers

CADE
1998
Springer

System Description: leanK 2.0

14 years 2 months ago
System Description: leanK 2.0
Abstract. 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. Overview. leanK is a "lean" Prolog implementation of the free variable tableau calculus for propositional modal logics reported in [1]. It performs depth first search and is based upon leanTAP [2]. Formulae are annotated with labels containing variables, which capture the universal and existential nature of the box and diamond modalities, respectively. leanK 2.0 includes additional search space restrictions and fairness strategies, giving a decision procedure for the logics K, KT, and S4. It has 87, 51, and 132 lines of code for K, KD, and S4, respectively. The main advantages of leanK are its modularity and its versatility. Due to its small size, leanK is easier to understand than a comp...
Bernhard Beckert, Rajeev Goré
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1998
Where CADE
Authors Bernhard Beckert, Rajeev Goré
Comments (0)