Theorem Proving and Model Building with the Calculus KE

A Prolog implementation of a new theorem-prover for first-order classical logic is described. The prover is based on the calculus KE and the rules used for analysing quantifiers in free variable semantic tableaux. A formal specification of the rules used in the implementation is described, for which soundness and completeness is straightforwardly verified. The prover has been tested on the first 47 problems of the Pelletier set, and its performance compared with a state of the art semantic tableaux theorem-prover. It has also been applied to model building in a prototype system for logical animation, a technique for symbolic execution which can be used for validation. The interest of these experiments is that they demonstrate the value of certain `characteristics' of the KE calculus, such as the significant space-saving in theorem-proving, the mutual inconsistency of open branches in KE trees, and the relation of the KE rules to `traditional' forms of reasoning. 1 Introduction 1.1 Ove..