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

• Type: Conference
• Year: 1995
• Where: AGP
• Authors: Alberto Artosi, Paola Cattabriga, Guido Governatori
• Keywords: AGP 1995, Artificial Intelligence, Label Formalism, Proof Search, Theorem Prover