TY - GEN

T1 - Category theoretic semantics for theorem proving in logic programming

T2 - 13th IFIP WG 1.3 International Workshop on Coalgebraic Methods in Computer Science, CMCS 2016 Colocated with Satellite Event of the Joint Conference on Theory and Practice of Software, ETAPS 2016

AU - Komendantskaya, Ekaterina

AU - Power, John

PY - 2016

Y1 - 2016

N2 - A propositional logic program P may be identified with a PfPf -coalgebra on the set of atomic propositions in the program. The corresponding C(PfPf)-coalgebra, where C(PfPf) is the cofree comonad on PfPf, 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.

AB - A propositional logic program P may be identified with a PfPf -coalgebra on the set of atomic propositions in the program. The corresponding C(PfPf)-coalgebra, where C(PfPf) is the cofree comonad on PfPf, 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.

KW - Coalgebra

KW - Coinductive derivation tree

KW - Kan extensions

KW - Lawvere theories

KW - Lax transformations

KW - Logic programming

KW - Term-matching resolution

UR - http://www.scopus.com/inward/record.url?scp=84976635909&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-40370-0_7

DO - 10.1007/978-3-319-40370-0_7

M3 - Conference contribution

AN - SCOPUS:84976635909

SN - 9783319403694

VL - 9608

T3 - Lecture Notes in Computer Science

SP - 94

EP - 113

BT - Coalgebraic Methods in Computer Science

A2 - Hasuo, Ichiro

PB - Springer

Y2 - 2 April 2016 through 3 April 2016

ER -