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.
Avellone, A., Ferrari, M., Fiorentini, C. (2001). A Formal Framework for Synthesis and Verification of Logic Programs. In K. Lau (a cura di), Logic Based Program Synthesis and Transformation (pp. 1-17). Springer Berlin Heidelberg [10.1007/3-540-45142-0_1].
A Formal Framework for Synthesis and Verification of Logic Programs
AVELLONE, ALESSANDRO;
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 | |
|---|---|---|---|
|
chp%3A10.1007%2F3-540-45142-0_1.pdf
Solo gestori archivio
Dimensione
272.14 kB
Formato
Adobe PDF
|
272.14 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
