A Prolog Implementation of Kem

12 years 3 months ago
A Prolog Implementation of Kem
In this paper, we describe a Prolog implementation of a new theorem prover for (normal propositional) modal and multi–modal logics. The theorem prover, which is called KEM, arises from the combination of a classical refutation system which incorporates a restricted (“analytic”) version of the cut rule with a label formalism which allows for a specialised, logic–dependent unification algorithm. An essential feature of KEM is that it yields a rather simple and efficient proof search procedure which offers many computational advantages over the usual tableau–based proof search methods. This is due partly to the use of linear 2–premise β rules in place of the branching β rules of the standard tableau method, and partly to the crucial role played by the analytic cut (the only branching rule) in eliminating redundancy from the search space. It turns out that KEM method of proof search is not only computationally more efficient but also intuitively more natural than other (e....
Alberto Artosi, Paola Cattabriga, Guido Governator
Added 25 Aug 2010
Updated 25 Aug 2010
Type Conference
Year 1995
Where AGP
Authors Alberto Artosi, Paola Cattabriga, Guido Governatori
Comments (0)