Proving Theorems by Mimicking a Human’s Skill

Acquisition, Learning, and Demonstration: Automating Tasks for Users

Volume

Papers from the 1996 AAAI Spring Symposium

Contents

We investigate the improvement of theorem proven by reusing previously computed proofs. We have developed and implemented the PLAGIATOR system which proves theorems by mathematical induction 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 interactions 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 (automated) 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.