Logic programming: laxness and saturation

DOI10.1016/J.JLAMP.2018.07.004MaRDI QIDQ1994355zbMATH OpenOpenAlexWikidataFDO

Authors Ekaterina Komendantskaya, John Power

Publication date 1 November 2018

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1608.07708

zbMATH Keywords

coalgebracoinductive derivation treeLawvere theoriesLax transformationslogic programmingsaturation

Mathematics Subject Classification ID

Theories (e.g., algebraic theories), structure, and semantics (18C10) Eilenberg-Moore and Kleisli constructions for monads (18C20) Logic programming (68N17)

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 programs with existential variables, and to develop a precise semantic relationship between variables in logic programming and worlds in local state.

Recommendations

• Logic programming with satisfiability
• scientific article; zbMATH DE number 65531
• The expressive powers of the logic programming semantics
• scientific article; zbMATH DE number 3866574
• On logical constraints in logic programming
• Logic programming and logarithmic space
• Logic programming with default, weak and strict negations
• Publication:3030254
• Complexity and undecidability results for logic programming

Cites work

• A category theoretic formulation for Engeler-style models of the untyped -calculus
• A productivity checker for logic programming
• A theory of observables for logic programs
• A type-theoretic approach to resolution
• An algebraic formulation for data refinement
• An interactive semantics of logic programming
• Bialgebraic semantics for logic programming
• Categorical semantics for programming languages
• Category theoretic semantics for theorem proving in logic programming: embracing the laxness
• Co-Logic Programming: Extending Logic Programming with Coinduction
• Coalgebraic derivations in logic programming
• Coalgebraic logic programming: from Semantics to Implementation
• Coalgebraic semantics for derivations in logic programming
• Coalgebraic semantics for parallel derivation strategies in logic programming
• Coinductive soundness of corecursive type class resolution
• Exploiting parallelism in coalgebraic logic programming
• scientific article; zbMATH DE number 3978351 (Why is no real title available?)
• scientific article; zbMATH DE number 3751225 (Why is no real title available?)
• scientific article; zbMATH DE number 43398 (Why is no real title available?)
• scientific article; zbMATH DE number 3522192 (Why is no real title available?)
• scientific article; zbMATH DE number 1314223 (Why is no real title available?)
• scientific article; zbMATH DE number 2087441 (Why is no real title available?)
• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• scientific article; zbMATH DE number 3367095 (Why is no real title available?)
• Introduction to bicategories
• Lax naturality through enrichment
• On the algebraic structure of declarative programming languages
• Operational semantics of resolution and productivity in Horn clause logic
• Productive corecursion in logic programming
• Proof relevant corecursive resolution
• Reactive systems, (semi-)saturated semantics and coalgebras on presheaves
• Saturated semantics for coalgebraic logic programming
• Structural resolution for logic programming
• Two-dimensional monad theory

Cited in

(6)

• Saturated semantics for coalgebraic logic programming
• Coalgebraic semantics for derivations in logic programming
• Coalgebraic semantics for probabilistic logic programming
• Category theoretic semantics for theorem proving in logic programming: embracing the laxness
• scientific article; zbMATH DE number 7649893 (Why is no real title available?)
• A Coalgebraic Approach to Unification Semantics of Logic Programming

Describes a project that uses

Uses Software

• CoALP

This page was built for publication: Logic programming: laxness and saturation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1994355)