Kolbe, Thomas ; Walther, Christoph (1995)
Adaption of Proofs for Reuse.
1995 Fall Symposium Adaptation of Knowledge for Reuse. Cambridge, USA (10.11.1995-12.11.1995)
Conference or Workshop Item, Bibliographie
Abstract
Automated theorem provers might be improved if they are enabled to reuse previously computed proofs. Our approach for reuse is based on generalizing computed proofs by replacing function symbols with function variables. This yields a schematic proof which is instantiated subsequently for obtaining proofs of new, similar conjectures. Our reuse method requires two steps of proof adaptation, viz. the solution of so-called free function variables and the patching of completely instantiated proofs. We develop algorithms for solving free function variables and for computing patched proofs and demonstrate their usefulness with several examples.
| Item Type: | Conference or Workshop Item |
|---|---|
| Erschienen: | 1995 |
| Creators: | Kolbe, Thomas ; Walther, Christoph |
| Type of entry: | Bibliographie |
| Title: | Adaption of Proofs for Reuse |
| Language: | English |
| Date: | 1995 |
| Place of Publication: | Cambridge, USA |
| Event Title: | 1995 Fall Symposium Adaptation of Knowledge for Reuse |
| Event Location: | Cambridge, USA |
| Event Dates: | 10.11.1995-12.11.1995 |
| URL / URN: | https://aaai.org/Library/Symposia/Fall/fs95-04.php |
| Corresponding Links: | |
| Abstract: | Automated theorem provers might be improved if they are enabled to reuse previously computed proofs. Our approach for reuse is based on generalizing computed proofs by replacing function symbols with function variables. This yields a schematic proof which is instantiated subsequently for obtaining proofs of new, similar conjectures. Our reuse method requires two steps of proof adaptation, viz. the solution of so-called free function variables and the patching of completely instantiated proofs. We develop algorithms for solving free function variables and for computing patched proofs and demonstrate their usefulness with several examples. |
| Divisions: | 20 Department of Computer Science 20 Department of Computer Science > Programming Methodology |
| Date Deposited: | 19 Nov 2008 15:58 |
| Last Modified: | 25 Apr 2024 08:55 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Send an inquiry |
Options (only for editors)
 |
Show editorial Details |
Drucken
Impressum