In this paper we present a formal framework, based on the notion of extraction calculus, which has been applied to define procedures for extracting information from constructive proofs. Here we 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.
A formal framework for synthesis and verification of logic programs / A. Avellone, M. Ferrari, C. Fiorentini - In: Logic based program synthesis and transformation : 10th international workshop, LOPSTR 2000 : London, UK, july 24-28, 2000 : selected papers / [a cura di] K. -K. Lau. - Berlin : Springer, 2001. - ISBN 3540421270. - pp. 1-17 (( Intervento presentato al 10. convegno International Workshop on Logic-based Program Synthesis and Transformation tenutosi a London nel 2000 [10.1007/3-540-45142-0_1].
A formal framework for synthesis and verification of logic programs
C. Fiorentini
2001
Abstract
In this paper we present a formal framework, based on the notion of extraction calculus, which has been applied to define procedures for extracting information from constructive proofs. Here we 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.
| File | Dimensione | Formato | |
|---|---|---|---|
|
2001_lopstr.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
272.14 kB
Formato
Adobe PDF
|
272.14 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
