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.
|Name||Leibniz International Proceedings in Informatics (LIPIcs)|
|Publisher||Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik|
- Logic programming
- Lawvere theoriesm
- coinductive logic programming
- concurrent logic programming