AAAI Conference 1984 Conference Paper
A Self-Modifying Theorem Prover
- Cynthia A. Brown
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.