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 Verlag [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.
Capitolo o saggio
program synthesis
English
Logic Based Program Synthesis and Transformation
Lau, Kung-Kiu
2-mag-2001
9783540421276
2042
Springer Verlag
1
17
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 Verlag [10.1007/3-540-45142-0_1].
reserved
File in questo prodotto:
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10281/53469
Citazioni
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 2
Social impact