TY - GEN
T1 - Constructing Induction Rules for Deductive Synthesis Proofs
AU - Bundy, Alan
AU - Dixon, Lucas
AU - Gow, Jeremy
AU - Fleuriot, Jacques
PY - 2005
Y1 - 2005
N2 - 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
AB - 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
KW - deductive synthesis
KW - proof planning
KW - induction
KW - theorem proving
KW - middle-out reasoning
U2 - 10.1016/j.entcs.2005.08.003
DO - 10.1016/j.entcs.2005.08.003
M3 - Conference contribution
VL - 153
T3 - Electronic Notes in Theoretical Computer Science
SP - 3
EP - 21
BT - Electronic Notes in Theoretical Computer Science
ER -