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.

• Type: Conference
• Year: 1990
• Where: AAAI
• Authors: Nachum Dershowitz, Eli Pinchover
• Keywords: AAAI 1990, Equational Approach, Intelligent Agents, Logic Programs, Program Contains Equations