TY - CHAP
T1 - Coalgebraic Derivations in Logic Programming
AU - Komendantskaya, Ekaterina
AU - Power, John
PY - 2011
Y1 - 2011
N2 - Coalgebra may be used to provide semantics for SLD-derivations, both finite and infinite. We first give such semantics to classical SLD-derivations, proving results such as adequacy, soundness and completeness. Then, based upon coalgebraic semantics, we propose a new sound and complete algorithm for parallel derivations. We analyse this new algorithm in terms of the Theory of Observables, and we prove soundness, completeness, correctness and full abstraction results.
AB - Coalgebra may be used to provide semantics for SLD-derivations, both finite and infinite. We first give such semantics to classical SLD-derivations, proving results such as adequacy, soundness and completeness. Then, based upon coalgebraic semantics, we propose a new sound and complete algorithm for parallel derivations. We analyse this new algorithm in terms of the Theory of Observables, and we prove soundness, completeness, correctness and full abstraction results.
KW - Logic programming
KW - SLD-resolution
KW - concurrency
KW - coinduction
KW - Lawvere theoriesm
KW - coinductive logic programming
KW - concurrent logic programming
UR - https://www.scopus.com/pages/publications/84880203100
U2 - 10.4230/LIPIcs.CSL.2011.352
DO - 10.4230/LIPIcs.CSL.2011.352
M3 - Chapter
SN - 9783939897323
T3 - Leibniz International Proceedings in Informatics (LIPIcs)
SP - 352
EP - 366
BT - Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL
PB - Schloss Dagstuhl - Leibniz-Zentrum für Informatik
ER -