Category Theoretic Semantics for Theorem Proving in Logic Programming: Embracing the Laxness - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2016

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

Résumé

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.
Fichier principal
Vignette du fichier
418352_1_En_7_Chapter.pdf (360.02 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01446035 , version 1 (25-01-2017)

Licence

Paternité

Identifiants

Citer

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⟩
97 Consultations
46 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More