| Publication type: |
Article in Proceedings |
| Author: |
Einar Broch Johnsen, Christoph Lüth |
| Editor: |
Konrad Slind, Annette Bunker, Ganesh Gopalakrishnan |
| Title: |
Theorem Reuse by Proof Term Transformation |
| Book / Collection title: |
International Conference on Theorem Proving in Higher-Order Logics TPHOLs 2004 |
| Volume: |
3223 |
| Page(s): |
152 – 167 |
| Series: |
Lecture Notes in Computer Science |
| Year published: |
2004 |
| Publisher: |
Springer |
| Abstract: |
Proof reuse addresses the issue of how proofs of theorems in a specific setting can be used to prove other theorems in different settings. This paper proposes an approach where theorems are generalised by abstracting their proofs from the original setting. The approach is based on a representation of proofs as logical framework proof terms, using the theorem prover Isabelle. The logical framework allows type-specific inference rules to be handled uniformly in the abstraction process and the prover's automated proof tactics may be used freely. This way, established results become more generally applicable; for example, theorems about a data type can be reapplied to other types. The paper also considers how to reapply such abstracted theorems, and suggests an approach based on mappings between operations and types, and on systematically exploiting the dependencies between theorems. |
| PDF Version: |
http://www.informatik.uni-bremen.de/~cxl/papers/tphols04.pdf |
| PostScript Version: |
http://www.informatik.uni-bremen.de/~cxl/papers/tphols04.ps.gz |
| Status: |
Reviewed |
| Last updated: |
25. 11. 2004 |
