An incompleteness result for deductive synthesis of logic programs
Kung-Kiu Lau, Mario Ornaghi · 1993
We formalise the derivation of logic programs from their specifications by deductive synthesis, and introduce the notion of uniform equivalence between logical systems. This enables us to present an incompleteness result for deductive synthesis of logic programs from first-order logic specifications. 1 Introduction Logic program synthesis was studied by some researchers in the early days of logic programming. Most notable among these are Clark, Hansson, Hogger, and Tarnlund. Automated (or semi-automated) synthesis, however, has only received serious attention much more recently. A preliminary survey, in the form of a catalogue, of logic program synthesis methods can be found in [8]. The goal of logic program synthesis is to systematically derive logic programs from their specifications. For example, in the proofs-as-programs approach, the specification takes the form of a theorem (or more accurately a conjecture) stating the existence of the required output for any legitimate input; a...