# 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 :
Type de document :
Communication dans un congrès
Ichiro Hasuo. 13th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2016, Eindhoven, Netherlands. Lecture Notes in Computer Science, LNCS-9608, pp.94-113, 2016, Coalgebraic Methods in Computer Science. 〈10.1007/978-3-319-40370-0_7〉
Domaine :

Littérature citée [33 références]

https://hal.inria.fr/hal-01446035
Contributeur : Hal Ifip <>
Soumis le : mercredi 25 janvier 2017 - 15:24:31
Dernière modification le : mercredi 4 octobre 2017 - 14:56:17
Document(s) archivé(s) le : mercredi 26 avril 2017 - 14:56:56

### Fichier

##### Accès restreint
Fichier visible le : 2019-01-01

Connectez-vous pour demander l'accès au fichier

### Citation

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

### Métriques

Consultations de la notice