Inductive Synthesis of Equational Programs

An equational approach to the synthesis of functional and logic programs is taken. Typically, a target program contains equations that are only true in the standard model of the given domain rules. To synthesize such programs, induction is necessary. We propose heuristics for generalizing from a sequence of deductive consequences. These are combined with rewrite-based methods of inductive proof to derive provably correct programs. a survey of rewriting, see (Dershowitz & Jouannaud 1990); for completion and its applications, see (Dershowitz 1989). Consider the following toy system S for addition and doubling (d) of natural numbers in unary notation: x+0 + x x + S(Y) + s(x+y) d(x) + x+x

Authors

• Nachum Dershowitz

Keywords

No keywords are indexed for this paper.