Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

AI

2000

Springer

2000

Springer

We investigate the improvement of theorem proving by reusing previously computed proofs. We have developed and implemented the PLAGIATOR system which proves theorems by mathematical induction with the aid of a human advisor: If a base or step formula is submitted to the system, it tries to reuse a proof of a previously verified formula. If successful, labour is saved, because the number of required user interactions is decreased. Otherwise the human advisor is called for providing a hand crafted proof for such a formula, which subsequently--after some (automated) preparation steps--is stored in the system's memory, to be in stock for future reasoning problems. Besides the potential savings of resources, the performance of the overall system is improved, because necessary lemmata might be speculated as the result of an attempt to reuse a proof. The success of the approach is based on our techniques for preparing given proofs as well as by our methods for retrieval and adaptation o...

Related Content

Added |
17 Dec 2010 |

Updated |
17 Dec 2010 |

Type |
Journal |

Year |
2000 |

Where |
AI |

Authors |
Christoph Walther, Thomas Kolbe |

Comments (0)