Category theoretic semantics for theorem proving in logic programming: embracing the laxness

Ekaterina  Komendantskaya; John Power

doi:10.1007/978-3-319-40370-0_7

Category theoretic semantics for theorem proving in logic programming: embracing the laxness

Ekaterina Komendantskaya, John Power

Department of Computer Science

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

1 Citation (SciVal)

159 Downloads (Pure)

Abstract

A propositional logic program P may be identified with a
P f P f -coalgebra on the set of atomic propositions in the program. The
corresponding C(P f P f )-coalgebra, where C(P f P f ) is the cofree comonad
on P f P 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 ap-
proach, we further extend it to arbitrary logic programs. We also exhibit
a refinement of Bonchi and Zanasi’s saturation semantics for logic pro-
gramming that complements lax semantics.

Original language	English
Title of host publication	Proceedings of Coalgebraic Methods in Computer Science
Subtitle of host publication	13th IFIP WG 1.3 International Workshop, CMCS 2016, Colocated with ETAPS 2016, Eindhoven, The Netherlands, April 2-3, 2016, Revised Selected Papers
Editors	Ichiro Hasuo
Publisher	Springer
Pages	94-113
Number of pages	20
ISBN (Print)	9783319403694
DOIs	https://doi.org/10.1007/978-3-319-40370-0_7
Publication status	Published - 4 Jun 2016

Publication series

Name	Lecture Notes in Computer Science
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Name
Volume	9608

Keywords

Logic programming, coalgebra, term-matching resolution, coinductive derivation tree, Lawvere theories, lax transformations, Kan extensions.

Access to Document

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

finalacceptedAccepted author manuscript, 360 KB

Cite this

Komendantskaya, E., & Power, J. (2016). Category theoretic semantics for theorem proving in logic programming: embracing the laxness. In I. Hasuo (Ed.), Proceedings of Coalgebraic Methods in Computer Science: 13th IFIP WG 1.3 International Workshop, CMCS 2016, Colocated with ETAPS 2016, Eindhoven, The Netherlands, April 2-3, 2016, Revised Selected Papers (pp. 94-113). (Lecture Notes in Computer Science). Springer. https://doi.org/10.1007/978-3-319-40370-0_7

Category theoretic semantics for theorem proving in logic programming: embracing the laxness. / Komendantskaya, Ekaterina ; Power, John.
Proceedings of Coalgebraic Methods in Computer Science: 13th IFIP WG 1.3 International Workshop, CMCS 2016, Colocated with ETAPS 2016, Eindhoven, The Netherlands, April 2-3, 2016, Revised Selected Papers. ed. / Ichiro Hasuo. Springer, 2016. p. 94-113 (Lecture Notes in Computer Science).

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

Komendantskaya, E & Power, J 2016, Category theoretic semantics for theorem proving in logic programming: embracing the laxness. in I Hasuo (ed.), Proceedings of Coalgebraic Methods in Computer Science: 13th IFIP WG 1.3 International Workshop, CMCS 2016, Colocated with ETAPS 2016, Eindhoven, The Netherlands, April 2-3, 2016, Revised Selected Papers. Lecture Notes in Computer Science, Springer, pp. 94-113. https://doi.org/10.1007/978-3-319-40370-0_7

Komendantskaya E, Power J. Category theoretic semantics for theorem proving in logic programming: embracing the laxness. In Hasuo I, editor, Proceedings of Coalgebraic Methods in Computer Science: 13th IFIP WG 1.3 International Workshop, CMCS 2016, Colocated with ETAPS 2016, Eindhoven, The Netherlands, April 2-3, 2016, Revised Selected Papers. Springer. 2016. p. 94-113. (Lecture Notes in Computer Science). Epub 2016 Jun 4. doi: 10.1007/978-3-319-40370-0_7

Komendantskaya, Ekaterina ; Power, John. / Category theoretic semantics for theorem proving in logic programming: embracing the laxness. Proceedings of Coalgebraic Methods in Computer Science: 13th IFIP WG 1.3 International Workshop, CMCS 2016, Colocated with ETAPS 2016, Eindhoven, The Netherlands, April 2-3, 2016, Revised Selected Papers. editor / Ichiro Hasuo. Springer, 2016. pp. 94-113 (Lecture Notes in Computer Science).

@inproceedings{d105fa93035f49cd8b91fe3df50827d3,

title = "Category theoretic semantics for theorem proving in logic programming: embracing the laxness",

abstract = "A propositional logic program P may be identified with aP f P f -coalgebra on the set of atomic propositions in the program. Thecorresponding C(P f P f )-coalgebra, where C(P f P f ) is the cofree comonadon P f P f , describes derivations by resolution. Using lax semantics, thatcorrespondence may be extended to a class of first-order logic programswithout existential variables. The resulting extension captures the proofsby term-matching resolution in logic programming. Refining the lax ap-proach, we further extend it to arbitrary logic programs. We also exhibita refinement of Bonchi and Zanasi{\textquoteright}s saturation semantics for logic pro-gramming that complements lax semantics.",

keywords = "Logic programming, coalgebra, term-matching resolution, coinductive derivation tree, Lawvere theories, lax transformations, Kan extensions.",

author = "Ekaterina Komendantskaya and John Power",

year = "2016",

month = jun,

day = "4",

doi = "10.1007/978-3-319-40370-0_7",

language = "English",

isbn = "9783319403694",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "94--113",

editor = "Ichiro Hasuo",

booktitle = "Proceedings of Coalgebraic Methods in Computer Science",

}

TY - GEN

T1 - Category theoretic semantics for theorem proving in logic programming: embracing the laxness

AU - Komendantskaya, Ekaterina

AU - Power, John

PY - 2016/6/4

Y1 - 2016/6/4

N2 - A propositional logic program P may be identified with aP f P f -coalgebra on the set of atomic propositions in the program. Thecorresponding C(P f P f )-coalgebra, where C(P f P f ) is the cofree comonadon P f P f , describes derivations by resolution. Using lax semantics, thatcorrespondence may be extended to a class of first-order logic programswithout existential variables. The resulting extension captures the proofsby term-matching resolution in logic programming. Refining the lax ap-proach, we further extend it to arbitrary logic programs. We also exhibita refinement of Bonchi and Zanasi’s saturation semantics for logic pro-gramming that complements lax semantics.

AB - A propositional logic program P may be identified with aP f P f -coalgebra on the set of atomic propositions in the program. Thecorresponding C(P f P f )-coalgebra, where C(P f P f ) is the cofree comonadon P f P f , describes derivations by resolution. Using lax semantics, thatcorrespondence may be extended to a class of first-order logic programswithout existential variables. The resulting extension captures the proofsby term-matching resolution in logic programming. Refining the lax ap-proach, we further extend it to arbitrary logic programs. We also exhibita refinement of Bonchi and Zanasi’s saturation semantics for logic pro-gramming that complements lax semantics.

KW - Logic programming, coalgebra, term-matching resolution, coinductive derivation tree, Lawvere theories, lax transformations, Kan extensions.

UR - http://dx.doi.org/10.1007/978-3-319-40370-0_7

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

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

M3 - Chapter in a published conference proceeding

SN - 9783319403694

T3 - Lecture Notes in Computer Science

SP - 94

EP - 113

BT - Proceedings of Coalgebraic Methods in Computer Science

A2 - Hasuo, Ichiro

PB - Springer

ER -

Category theoretic semantics for theorem proving in logic programming: embracing the laxness

Abstract

Publication series

Keywords

Access to Document

Other files and links

Fingerprint

Coalgebraic Logic Programming for Type Inference

Cite this

Category theoretic semantics for theorem proving in logic programming: embracing the laxness

Abstract

Publication series

Keywords

Access to Document

Other files and links

Fingerprint

Projects

Coalgebraic Logic Programming for Type Inference

Cite this