Coalgebraic Derivations in Logic Programming

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 correctness and full abstraction results.

Authors

• Ekaterina Komendantskaya
• John Power

Keywords

• Logic programming
• SLD-resolution
• concurrency
• coinduction
• Lawvere theoriesm
• coinductive logic programming
• concurrent logic programming