Category theoretic semantics for theorem proving in logic programming: embracing the laxness

Ekaterina Komendantskaya, John Power

Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding

1 Citation (SciVal)
142 Downloads (Pure)


A propositional logic program P may be identified with a
P f P f -coalgebra on the set of atomic propositions in the program. The
corresponding C(P f P f )-coalgebra, where C(P f P f ) is the cofree comonad
on P f P f , describes derivations by resolution. Using lax semantics, that
correspondence may be extended to a class of first-order logic programs
without existential variables. The resulting extension captures the proofs
by term-matching resolution in logic programming. Refining the lax ap-
proach, we further extend it to arbitrary logic programs. We also exhibit
a refinement of Bonchi and Zanasi’s saturation semantics for logic pro-
gramming that complements lax semantics.
Original languageEnglish
Title of host publicationProceedings of Coalgebraic Methods in Computer Science
Subtitle of host publication13th IFIP WG 1.3 International Workshop, CMCS 2016, Colocated with ETAPS 2016, Eindhoven, The Netherlands, April 2-3, 2016, Revised Selected Papers
EditorsIchiro Hasuo
Number of pages20
ISBN (Print)9783319403694
Publication statusPublished - 4 Jun 2016

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


  • Logic programming, coalgebra, term-matching resolution, coinductive derivation tree, Lawvere theories, lax transformations, Kan extensions.


Dive into the research topics of 'Category theoretic semantics for theorem proving in logic programming: embracing the laxness'. Together they form a unique fingerprint.

Cite this