### Abstract

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 language | English |
---|---|

Pages (from-to) | 1-21 |

Number of pages | 21 |

Journal | Journal of Logical and Algebraic Methods in Programming |

Volume | 101 |

Early online date | 19 Jul 2018 |

DOIs | |

Publication status | Published - 31 Dec 2018 |

### Fingerprint

### Keywords

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

### Cite this

*Journal of Logical and Algebraic Methods in Programming*,

*101*, 1-21. https://doi.org/10.1016/j.jlamp.2018.07.004

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

Research output: Contribution to journal › Article

*Journal of Logical and Algebraic Methods in Programming*, vol. 101, pp. 1-21. https://doi.org/10.1016/j.jlamp.2018.07.004

}

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 -