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

1 Citation (Scopus)
124 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 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
Number of pages20
ISBN (Print)9783319403694
DOIs
Publication statusPublished - 4 Jun 2016

Publication series

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

Keywords

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

Fingerprint Dive into the research topics of 'Category theoretic semantics for theorem proving in logic programming: embracing the laxness'. Together they form a unique fingerprint.

  • Projects

  • 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