Coalgebraic Derivations in Logic Programming

Research output: Chapter in Book/Report/Conference proceedingChapter

13 Citations (Scopus)
34 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationComputer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL
PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
Number of pages15
ISBN (Print)9783939897323
Publication statusPublished - 2011

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dagstuhl - Leibniz-Zentrum fuer Informatik
ISSN (Print)1868-8969


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


Dive into the research topics of 'Coalgebraic Derivations in Logic Programming'. Together they form a unique fingerprint.

Cite this