Kolbe, Thomas ; Walther, Christoph (1995)
Adaption of Proofs for Reuse.
1995 Fall Symposium Adaptation of Knowledge for Reuse. Cambridge, USA (10.11.-12.11.1995)
Konferenzveröffentlichung, Bibliographie
Kurzbeschreibung (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.
| Typ des Eintrags: | Konferenzveröffentlichung |
|---|---|
| Erschienen: | 1995 |
| Autor(en): | Kolbe, Thomas ; Walther, Christoph |
| Art des Eintrags: | Bibliographie |
| Titel: | Adaption of Proofs for Reuse |
| Sprache: | Englisch |
| Publikationsjahr: | 1995 |
| Ort: | Cambridge, USA |
| Veranstaltungstitel: | 1995 Fall Symposium Adaptation of Knowledge for Reuse |
| Veranstaltungsort: | Cambridge, USA |
| Veranstaltungsdatum: | 10.11.-12.11.1995 |
| URL / URN: | https://aaai.org/Library/Symposia/Fall/fs95-04.php |
| Zugehörige Links: | |
| Kurzbeschreibung (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. |
| Fachbereich(e)/-gebiet(e): | 20 Fachbereich Informatik 20 Fachbereich Informatik > Programmiermethodik |
| Hinterlegungsdatum: | 19 Nov 2008 15:58 |
| Letzte Änderung: | 25 Apr 2024 08:55 |
| PPN: | |
| Zugehörige Links: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum