Projects per year
Abstract
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 firstorder logic programs
without existential variables. The resulting extension captures the proofs
by termmatching 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.
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 firstorder logic programs
without existential variables. The resulting extension captures the proofs
by termmatching 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 language  English 

Title of host publication  Proceedings of Coalgebraic Methods in Computer Science 
Subtitle of host publication  13th IFIP WG 1.3 International Workshop, CMCS 2016, Colocated with ETAPS 2016, Eindhoven, The Netherlands, April 23, 2016, Revised Selected Papers 
Editors  Ichiro Hasuo 
Publisher  Springer 
Pages  94113 
Number of pages  20 
ISBN (Print)  9783319403694 
DOIs  
Publication status  Published  4 Jun 2016 
Publication series
Name  Lecture Notes in Computer Science 

ISSN (Print)  03029743 
ISSN (Electronic)  16113349 
Name  

Volume  9608 
Keywords
 Logic programming, coalgebra, termmatching resolution, coinductive derivation tree, Lawvere theories, lax transformations, Kan extensions.
Fingerprint
Dive into the research topics of 'Category theoretic semantics for theorem proving in logic programming: embracing the laxness'. Together they form a unique fingerprint.Projects
 1 Finished

Coalgebraic Logic Programming for Type Inference
Power, J. (PI)
Engineering and Physical Sciences Research Council
1/09/13 → 31/01/17
Project: Research council