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

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

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’s saturation semantics for logic programming that complements lax semantics.

Original languageEnglish
Title of host publicationCoalgebraic 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 International Publishing
Pages94-113
Number of pages20
Volume9608
ISBN (Electronic)9783319403700
ISBN (Print)9783319403694
DOIs
Publication statusPublished - 2016
Event13th 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 20163 Apr 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer International Publishing
Volume9608
ISSN (Print)0302-9743

Conference

Conference13th 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
CountryNetherlands
CityEindhoven
Period2/04/163/04/16

Keywords

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

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

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.

  • 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 International Publishing. https://doi.org/10.1007/978-3-319-40370-0_7