I present the Whelk proof development system, a tool for the synthesis and transformation of
logic programs. Whelk is based on ideas used in the “Proofs-as-Programs” literature| 9, 1],
which enable the extraction of logic programs from proofs, in a similar way to that of [10].
Using Whelk, we can synthesise pure logic programs|| 4|| which may be easily translated
into “real” logic programming languages such as Prolog and Gödel. Delay declarations to
prevent floundering and unbounded recursion may also be generated automatically. In the …