Logic programming: laxness and saturation

Ekaterina Komendantskaya, Anthony Power

Research output: Contribution to journalArticle

9 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. That correspondence has been developed to model first-order programs in two ways, with lax semantics and saturated semantics, based on locally ordered categories and right Kan extensions respectively. We unify the two approaches, exhibiting them as complementary rather than competing, reflecting the theorem-proving and proof-search aspects of logic programming. While maintaining that unity, we further refine lax semantics to give finitary models of logic progams with existential variables, and to develop a precise semantic relationship between variables in logic programming and worlds in local state.
Original languageEnglish
Pages (from-to)1-21
Number of pages21
JournalJournal of Logical and Algebraic Methods in Programming
Volume101
Early online date19 Jul 2018
DOIs
Publication statusPublished - 31 Dec 2018

Fingerprint

Logic programming
Logic Programming
Saturation
Semantics
Coalgebra
Ordered Categories
Proof Search
Theorem proving
Theorem Proving
Propositional Logic
Logic Programs
Proposition
Correspondence
Logic
First-order
Model

Keywords

  • Logic programming, coalgebra, coinductive derivation tree, Lawvere theories, lax transformations, saturation

Cite this

Logic programming: laxness and saturation. / Komendantskaya, Ekaterina ; Power, Anthony.

In: Journal of Logical and Algebraic Methods in Programming, Vol. 101, 31.12.2018, p. 1-21.

Research output: Contribution to journalArticle

Komendantskaya, Ekaterina ; Power, Anthony. / Logic programming: laxness and saturation. In: Journal of Logical and Algebraic Methods in Programming. 2018 ; Vol. 101. pp. 1-21.
@article{f5f0787fdf9846bc81a989259bdcd3be,
title = "Logic programming: laxness and saturation",
abstract = "A propositional logic program P may be identified with a P f P f -coalgebra onthe 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. That correspondence has been developed to model first-order programs in two ways, with lax semantics and saturated semantics, based on locally ordered categories and right Kan extensions respectively. We unify the two approaches, exhibiting them as complementary rather than competing, reflecting the theorem-proving and proof-search aspects of logic programming. While maintaining that unity, we further refine lax semantics to give finitary models of logic progams with existential variables, and to develop a precise semantic relationship between variables in logic programming and worlds in local state.",
keywords = "Logic programming, coalgebra, coinductive derivation tree, Lawvere theories, lax transformations, saturation",
author = "Ekaterina Komendantskaya and Anthony Power",
year = "2018",
month = "12",
day = "31",
doi = "10.1016/j.jlamp.2018.07.004",
language = "English",
volume = "101",
pages = "1--21",
journal = "Journal of Logical and Algebraic Methods in Programming",
issn = "2352-2208",
publisher = "Elsevier",

}

TY - JOUR

T1 - Logic programming: laxness and saturation

AU - Komendantskaya, Ekaterina

AU - Power, Anthony

PY - 2018/12/31

Y1 - 2018/12/31

N2 - A propositional logic program P may be identified with a P f P f -coalgebra onthe 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. That correspondence has been developed to model first-order programs in two ways, with lax semantics and saturated semantics, based on locally ordered categories and right Kan extensions respectively. We unify the two approaches, exhibiting them as complementary rather than competing, reflecting the theorem-proving and proof-search aspects of logic programming. While maintaining that unity, we further refine lax semantics to give finitary models of logic progams with existential variables, and to develop a precise semantic relationship between variables in logic programming and worlds in local state.

AB - A propositional logic program P may be identified with a P f P f -coalgebra onthe 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. That correspondence has been developed to model first-order programs in two ways, with lax semantics and saturated semantics, based on locally ordered categories and right Kan extensions respectively. We unify the two approaches, exhibiting them as complementary rather than competing, reflecting the theorem-proving and proof-search aspects of logic programming. While maintaining that unity, we further refine lax semantics to give finitary models of logic progams with existential variables, and to develop a precise semantic relationship between variables in logic programming and worlds in local state.

KW - Logic programming, coalgebra, coinductive derivation tree, Lawvere theories, lax transformations, saturation

U2 - 10.1016/j.jlamp.2018.07.004

DO - 10.1016/j.jlamp.2018.07.004

M3 - Article

VL - 101

SP - 1

EP - 21

JO - Journal of Logical and Algebraic Methods in Programming

JF - Journal of Logical and Algebraic Methods in Programming

SN - 2352-2208

ER -