# Category Theoretic Semantics for Theorem Proving in Logic Programming: Embracing the Laxness

Abstract : 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.
Keywords :
Document type :
Conference papers
Domain :

Cited literature [33 references]

https://hal.inria.fr/hal-01446035
Contributor : Hal Ifip <>
Submitted on : Wednesday, January 25, 2017 - 3:24:31 PM
Last modification on : Wednesday, October 4, 2017 - 2:56:17 PM
Long-term archiving on : Wednesday, April 26, 2017 - 2:56:56 PM

### File

418352_1_En_7_Chapter.pdf
Files produced by the author(s)

### Citation

Ekaterina Komendantskaya, John Power. Category Theoretic Semantics for Theorem Proving in Logic Programming: Embracing the Laxness. 13th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2016, Eindhoven, Netherlands. pp.94-113, ⟨10.1007/978-3-319-40370-0_7⟩. ⟨hal-01446035⟩

Record views