Category Theoretic Semantics for Theorem Proving in Logic Programming: Embracing the Laxness

DOI10.1007/978-3-319-40370-0_7zbMath1475.68055arXiv1602.05400OpenAlexW2288108789MaRDI QIDQ5739451

Ekaterina Komendantskaya, A. 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

coalgebralogic programmingKan extensionsLawvere theoriescoinductive derivation treelax transformationsterm-matching resolution

Mathematics Subject Classification ID

Logic programming (68N17) Categorical semantics of formal languages (18C50)

Related Items

Logic programming: laxness and saturation

Uses Software

• CoALP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Exploiting parallelism in coalgebraic logic programming
• Reactive systems, (semi-)saturated semantics and coalgebras on presheaves
• On the algebraic structure of declarative programming languages
• Two-dimensional monad theory
• A theory of observables for logic programs
• Lax naturality through enrichment
• Reports of the Midwest Category Seminar
• The formal theory of monads
• Proof Relevant Corecursive Resolution
• Saturated Semantics for Coalgebraic Logic Programming
• Coalgebraic Derivations in Logic Programming
• Coalgebraic Semantics for Parallel Derivation Strategies in Logic Programming
• Coalgebraic Semantics for Derivations in Logic Programming
• An interactive semantics of logic programming
• Bialgebraic Semantics for Logic Programming
• Co-Logic Programming: Extending Logic Programming with Coinduction
• Coalgebraic logic programming: from Semantics to Implementation
• A Type-Theoretic Approach to Resolution