TU Darmstadt / ULB / TUbiblio

Adaption of Proofs for Reuse

Kolbe, Thomas ; Walther, Christoph (1995):
Adaption of Proofs for Reuse.
1995 Fall Symposium Adaptation of Knowledge for Reuse, Cambridge, USA, 10.-12.11., [Conference or Workshop Item]

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
Title: Adaption of Proofs for Reuse
Language: English
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
Event Title: 1995 Fall Symposium Adaptation of Knowledge for Reuse
Event Location: Cambridge, USA
Event Dates: 10.-12.11.
Date Deposited: 19 Nov 2008 15:58
Official URL: https://aaai.org/Library/Symposia/Fall/fs95-04.php
License: [undefiniert]
Corresponding Links:
Export:
Suche nach Titel in: TUfind oder in Google
Send an inquiry Send an inquiry

Options (only for editors)
Show editorial Details Show editorial Details