%0 Conference Proceedings
%T Category Theoretic Semantics for Theorem Proving in Logic Programming: Embracing the Laxness
%+ Heriot-Watt University [Edinburgh] (HWU)
%+ University of Bath [Bath]
%A Komendantskaya, Ekaterina
%A Power, John
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 13th International Workshop on Coalgebraic Methods in Computer Science (CMCS)
%C Eindhoven, Netherlands
%Y Ichiro Hasuo
%3 Coalgebraic Methods in Computer Science
%V LNCS-9608
%P 94-113
%8 2016-04-02
%D 2016
%R 10.1007/978-3-319-40370-0_7
%K Logic programming
%K Coalgebra
%K Term-matching resolution
%K Coinductive derivation tree
%K Lawvere theories
%K Lax transformations
%K Kan extensions
%Z Computer Science [cs]Conference papers
%X A propositional logic program P may be identified with a $P_fP_f$-coalgebra on the set of atomic propositions in the program. The corresponding $C(P_fP_f)$-coalgebra, where $C(P_fP_f)$ is the cofree comonad on $P_fP_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 approach, we further extend it to arbitrary logic programs. We also exhibit a refinement of Bonchi and Zanasi’s saturation semantics for logic programming that complements lax semantics.
%G English
%Z TC 1
%Z WG 1.3
%2 https://inria.hal.science/hal-01446035/document
%2 https://inria.hal.science/hal-01446035/file/418352_1_En_7_Chapter.pdf
%L hal-01446035
%U https://inria.hal.science/hal-01446035
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-TC1
%~ IFIP-LNCS-9608
%~ IFIP-WG1-3
%~ IFIP-CMCS