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...

• Type: Conference
• Year: 1998
• Where: CADE
• Authors: Bernhard Beckert, Rajeev Goré
• Keywords: CADE 1998, Logical Reasoning, Modal Logics, Search Space Restrictions, Variable Tableau Calculus