Sciweavers

ENTCS
2006

Constructing Induction Rules for Deductive Synthesis Proofs

13 years 3 months ago
Constructing Induction Rules for Deductive Synthesis Proofs
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. Key words: deductive synthesis, proof planning, induction, theorem proving, middle-out reasoning.
Alan Bundy, Lucas Dixon, Jeremy Gow, Jacques D. Fl
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where ENTCS
Authors Alan Bundy, Lucas Dixon, Jeremy Gow, Jacques D. Fleuriot
Comments (0)