Proving Theorems by Mimicking a Human's Skill
Thomas H. Kolbe, Christoph Walther · TUbilio (Technical University of Darmstadt) · 1996
Abstract. x We investigate the improvement of the-orem proven by reusing previously computed proofs. We have developed and implemented the PLAGIATOR system which proves theorems by mathematical induc-tion with the aid ors human advisor: If a conjecture is submitted to the system, it tries to reuse a proof of a previously verified conjecture. If successful, resources are saved, because the n,,mhex of required user inter-actions is decreased. The pexfonnance of the overall system is improved, because neceuory lernmata might be specu/ated. If the reuse fails, the human advisor is called for providing a hand cxafted proof for such a conjecture, which subsequently-- after some (auto-mated) preparation steps m is stored in the system’s memory, to be in stock for future reasoning problems. The success of out approach is based on our te~h,,;que for preparing given proofs as well as by our techn/que for reusing proofs.