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

DOI10.1007/978-3-319-40370-0_7MaRDI QIDQ5739451zbMATH OpenOpenAlexFDO

Authors Ekaterina Komendantskaya, John Power

Publication date 15 July 2016

Published in Coalgebraic Methods in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

coalgebracoinductive derivation treeKan extensionsLawvere theorieslax transformationslogic programmingterm-matching resolution

Mathematics Subject Classification ID

Categorical semantics of formal languages (18C50) 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. 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.

Recommendations

• Logic programming: laxness and saturation
• Coalgebraic semantics for derivations in logic programming
• Coalgebraic semantics for parallel derivation strategies in logic programming
• Saturated semantics for coalgebraic logic programming
• scientific article; zbMATH DE number 2079032

Cites work

• A theory of observables for logic programs
• A type-theoretic approach to resolution
• An interactive semantics of logic programming
• Bialgebraic semantics for logic programming
• 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
• Exploiting parallelism in coalgebraic logic programming
• scientific article; zbMATH DE number 1705158 (Why is no real title available?)
• 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 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?)
• Lax naturality through enrichment
• On the algebraic structure of declarative programming languages
• Proof relevant corecursive resolution
• Reactive systems, (semi-)saturated semantics and coalgebras on presheaves
• Reports of the Midwest Category Seminar
• Saturated semantics for coalgebraic logic programming
• The formal theory of monads
• Two-dimensional monad theory

Cited in

(3)

• Logic programming: laxness and saturation
• Full Lambek Hyperdoctrine: Categorical Semantics for First-Order Substructural Logics
• Coalgebraic semantics for derivations in logic programming

Describes a project that uses

Uses Software

• CoALP

This page was built for publication: Category theoretic semantics for theorem proving in logic programming: embracing the laxness

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