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.
UR - http://www.scopus.com/inward/record.url?scp=84880203100&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.CSL.2011.352
DO - 10.4230/LIPIcs.CSL.2011.352
M3 - Chapter
AN - SCOPUS:84880203100
SN - 9783939897323
VL - 12
SP - 352
EP - 366
BT - Leibniz International Proceedings in Informatics, LIPIcs
PB - Dagstuhl Publications
ER -