The Markgraf Karl Refutation Procedure

Abstract

The current state of a Theorem Proving System (The Markgraf Karl Refutation Procedure) at the University of Karlsruhe is presented. The goal of this project can be summarized by the following three claims: it is possible to program a theorem prover (TP) and augment it by appropriate heuristics and domain-specific knowledge such that (i) it will display an 'active' and directed behaviour in its striving for a proof, rather than the 'passive' combinatorial search through very large search spaces, which was the characteristic behaviour of the TPs of the past. Consequently. (ii) it will not generate a search space of many thousands of irrelevant clauses, but will find a proof with comparatively few redundant derivation steps. (iii) Such a TP will establish an unprecedented leap in performance over previous TPs expressed in terms of the difficulty of the theorems it can prove. The results obtained thus far corroborate the first two claims.