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.
Citazione: | 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. |
Titolo: | A Formal Framework for Synthesis and Verification of Logic Programs |
Autori: | Avellone, A; Ferrari, M; Fiorentini, C |
Autori: | |
Presenza di un coautore afferente ad Istituzioni straniere: | No |
Tipo: | Capitolo o saggio |
Carattere della pubblicazione: | Scientifica |
Data di pubblicazione: | 2-mag-2001 |
Lingua: | English |
Titolo del libro: | Logic Based Program Synthesis and Transformation |
ISBN: | 978-3-540-42127-6 |
Appare nelle tipologie: | 03 - Contributo in libro |
File in questo prodotto:
File | Descrizione | Tipologia | Licenza | |
---|---|---|---|---|
chp%3A10.1007%2F3-540-45142-0_1.pdf | N/A | Administrator Richiedi una copia |