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

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

1 Citation (Scopus)

Abstract

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

Original language	English
Title of host publication	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
Volume	9608
ISBN (Electronic)	9783319403700
ISBN (Print)	9783319403694
DOIs	https://doi.org/10.1007/978-3-319-40370-0_7
Publication status	Published - 2016
Event	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 - Eindhoven, Netherlands Duration: 2 Apr 2016 → 3 Apr 2016

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer International Publishing
Volume	9608
ISSN (Print)	0302-9743

Conference

Conference	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
Country/Territory	Netherlands
City	Eindhoven
Period	2/04/16 → 3/04/16

Keywords

Coalgebra
Coinductive derivation tree
Kan extensions
Lawvere theories
Lax transformations
Logic programming
Term-matching resolution

ASJC Scopus subject areas

General Computer Science
Theoretical Computer Science

Access to Document

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

Cite this

Komendantskaya, E., & Power, J. (2016). Category theoretic semantics for theorem proving in logic programming: Embracing the laxness. In I. Hasuo (Ed.), 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 (Vol. 9608, pp. 94-113). (Lecture Notes in Computer Science; Vol. 9608). Springer. https://doi.org/10.1007/978-3-319-40370-0_7

Komendantskaya, Ekaterina ; Power, John. / Category theoretic semantics for theorem proving in logic programming : Embracing the laxness. 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. Vol. 9608 Springer, 2016. pp. 94-113 (Lecture Notes in Computer Science).

@inproceedings{a503dd6c6e104054a5e99285c04d30ba,

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

abstract = "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{\textquoteright}s saturation semantics for logic programming that complements lax semantics.",

keywords = "Coalgebra, Coinductive derivation tree, Kan extensions, Lawvere theories, Lax transformations, Logic programming, Term-matching resolution",

author = "Ekaterina Komendantskaya and John Power",

year = "2016",

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

language = "English",

isbn = "9783319403694",

volume = "9608",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "94--113",

editor = "Ichiro Hasuo",

booktitle = "Coalgebraic Methods in Computer Science",

note = "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 ; Conference date: 02-04-2016 Through 03-04-2016",

}

Komendantskaya, E & Power, J 2016, Category theoretic semantics for theorem proving in logic programming: Embracing the laxness. in I Hasuo (ed.), 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. vol. 9608, Lecture Notes in Computer Science, vol. 9608, Springer, pp. 94-113, 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, Eindhoven, Netherlands, 2/04/16. 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.
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. Vol. 9608 Springer, 2016. p. 94-113 (Lecture Notes in Computer Science; Vol. 9608).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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 -

Komendantskaya E, Power J. Category theoretic semantics for theorem proving in logic programming: Embracing the laxness. In Hasuo I, editor, 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. Vol. 9608. Springer. 2016. p. 94-113. (Lecture Notes in Computer Science). doi: 10.1007/978-3-319-40370-0_7

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

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this