Inductive Synthesis of Equational Programs

Nachum Dershowitz, Eli Pinchover

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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.