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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.