A formal framework for synthesis and verification of logic programs

In this paper we will present a formal framework, based on the notion of extraction calculus, which has been successfully applied to define procedures for extracting information from constructive proofs. Here we will apply such a mechanism to give a proof-theoretic account of SLD-derivations. We show how proofs of suitable constructive systems can be used in the context of deductive synthesis of logic programs, and we state a link between constructive and deductive program synthesis.

• Type: Conference
• Year: 2000
• Where: LOPSTR
• Authors: Alessandro Avellone, Mauro Ferrari, Camillo Fiorentini
• Keywords: Automated Reasoning, Constructive Proofs, Deductive Program Synthesis, LOPSTR 2000, Suitable Constructive Systems