Sciweavers

LOPSTR
2000
Springer

A formal framework for synthesis and verification of logic programs

13 years 7 months ago
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.
Alessandro Avellone, Mauro Ferrari, Camillo Fioren
Added 25 Aug 2010
Updated 25 Aug 2010
Type Conference
Year 2000
Where LOPSTR
Authors Alessandro Avellone, Mauro Ferrari, Camillo Fiorentini
Comments (0)