A Self-Modifying Theorem Prover

Abstract

Theorem provers can be viewed as containing declarative knowledge (in the form of axioms and lemmas) and procedural knowledge (in the form of an algorithm for proving theorems). Sometimes, as in the case of commutative laws in a Knuth-Bendix prover, it is appropriate or necessary to transfer knowledge from one category to the other. We describe a theorem proving system that independently recognizes opportunities for such transfers and performs them dynamically. Theorem proving algorithms Theorem provers can be divided into two general classes: those that operate without human intervention to prove straightforward consequences of a set of axioms, and those that serve as a