Coalgebraic Semantics for Derivations in Logic Programming

Research output: Chapter in Book/Report/Conference proceedingChapter

18 Citations (Scopus)


Every variable-free logic program induces a P P -coalgebra on the set of atomic formulae in the program. The coalgebra p sends an atomic formula A to the set of the sets of atomic formulae in the antecedent of each clause for which A is the head. In an earlier paper, we identified a variable-free logic program with a P P -coalgebra on Set and showed that, if C(P P ) is the cofree comonad on P P , then given a logic program P qua P P -coalgebra, the corresponding C(P P )-coalgebra structure describes the parallel and-or derivation trees of P. In this paper, we extend that analysis to arbitrary logic programs. That requires a subtle analysis of lax natural transformations between Poset-valued functors on a Lawvere theory, of locally ordered endofunctors and comonads on locally ordered categories, and of coalgebras, oplax maps of coalgebras, and the relationships between such for locally ordered endofunctors and the cofree comonads on them.
Original languageEnglish
Title of host publicationAlgebra and Coalgebra in Computer Science
Subtitle of host publication4th International Conference, CALCO 2011, Winchester, UK, August 30 – September 2, 2011. Proceedings
EditorsAndrea Corradini, Bartek Klin, Corina Cîrstea
Number of pages15
ISBN (Electronic)9783642229442
ISBN (Print)9783642229435
Publication statusPublished - 2011

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743


  • Logic programming
  • SLD-resolution
  • Coalgebra
  • Lawvere theories
  • Lax natural transformations
  • Oplax maps of coalgebras


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

Cite this