Logic program synthesis in a higherorder setting

Abstract. We describe a system for the synthesis of logic programs from specications based on higher-order logical descriptions of appro-priate renement operations. The system has been implemented within the proof planning system Clam. The generality of the approach is such that its extension to allow synthesis of higher-order logic programs was straightforward. Some illustrative examples are given. The approach is extensible to further classes of synthesis.