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

Ekaterina Komendantskaya, John Power

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
LanguageEnglish
Title of host publicationProceedings of Coalgebraic Methods in Computer Science
Subtitle of host publication13th IFIP WG 1.3 International Workshop, CMCS 2016, Colocated with ETAPS 2016, Eindhoven, The Netherlands, April 2-3, 2016, Revised Selected Papers
EditorsIchiro Hasuo
PublisherSpringer
Pages94-113
ISBN (Print)9783319403694
DOIs
StatusPublished - 4 Jun 2016

Publication series

NameLecture Notes in Computer Science
Name
Volume9608

Fingerprint

Theorem Proving
Logic Programming
Logic Programs
Coalgebra
Propositional Logic
First-order Logic
Proposition
Saturation
Refinement
Correspondence
Complement
Logic
Arbitrary
Term
Semantics

Keywords

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

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. DOI: 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 in Book/Report/Conference proceedingConference contribution

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. DOI: 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). Available from, 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’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 = "6",
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 - Conference contribution

SN - 9783319403694

T3 - Lecture Notes in Computer Science

SP - 94

EP - 113

BT - Proceedings of Coalgebraic Methods in Computer Science

PB - Springer

ER -