|
Informatics Report Series
|
|
|
|
|
|
|
|
|
| Title:Constructing Induction Rules for Deductive Synthesis Proofs |
| Authors:
Alan Bundy
; Lucas Dixon
; Jeremy Gow
; Jacques Fleuriot
|
| Date: 2005 |
| Publication Title:Proceedings of the Workshop on the Constructive Logic for Automated Software Engineering (CLASE 2005), Electronic Notes in Theoretical Computer Science |
|
Publication Type:Conference Paper
|
|
Volume No:153(1)
Page Nos:3-21
|
|
|
- Abstract:
-
We describe novel computational techniques for constructing induction rules for deductive synthesis proofs. Deductive synthesis holds out the promise of automated construction of correct computer programs from specifications of their desired behaviour. Synthesis of programs with iteration or recursion requires inductive proof, but standard techniques for the construction of appropriate induction rules are restricted to recycling the recursive structure of the specifications. What is needed is induction rule construction techniques that can introduce novel recursive structures. We show that a combination of rippling and the use of meta-variables as a least-commitment device can provide such novelty.
- Links To Paper
- 1st Link
- Bibtex format
- @InProceedings{EDI-INF-RR-0491,
- author = {
Alan Bundy
and Lucas Dixon
and Jeremy Gow
and Jacques Fleuriot
},
- title = {Constructing Induction Rules for Deductive Synthesis Proofs},
- book title = {Proceedings of the Workshop on the Constructive Logic for Automated Software Engineering (CLASE 2005), Electronic Notes in Theoretical Computer Science},
- year = 2005,
- volume = {153(1)},
- pages = {3-21},
- url = {http://dx.doi.org/10.1016/j.entcs.2005.08.003},
- }
|
