Coalgebraic logic programming: from Semantics to Implementation
From MaRDI portal
Abstract: Coinductive definitions, such as that of an infinite stream, may often be described by elegant logic programs, but ones for which SLD-refutation is of no value as SLD-derivations fall into infinite loops. Such definitions give rise to questions of lazy corecursive derivations and parallelism, as execution of such logic programs can have both recursive and corecursive features at once. Observational and coalgebraic semantics have been used to study them abstractly. The programming developments have often occurred separately and have usually been implementation-led. Here, we give a coherent semantics-led account of the issues, starting with abstract category theoretic semantics, developing coalgebra to characterise naturally arising trees, and proceeding towards implementation of a new dialect, CoALP, of logic programming, characterised by guarded lazy corecursion and parallelism.
Recommendations
- Coalgebraic derivations in logic programming
- Coalgebraic semantics for derivations in logic programming
- Coalgebraic semantics for parallel derivation strategies in logic programming
- Saturated semantics for coalgebraic logic programming
- A theoretical perspective of coinductive logic programming
- Coinductive Logic Programming and Its Applications
- Co-Logic Programming: Extending Logic Programming with Coinduction
- Coalgebraic semantics for probabilistic logic programming
- scientific article; zbMATH DE number 1753205
- Coalgebraic logic
Cited in
(25)- Logic programming: laxness and saturation
- Enhancing expressivity of checked corecursive streams
- On dual programs in co-logic programming and the Horn \({\mu}\)-calculus
- Operational semantics of resolution and productivity in Horn clause logic
- The coalgebraic class specification language CCSL
- CoALP
- Exploiting parallelism in coalgebraic logic programming
- A coalgebraic decision procedure for NetKAT
- Coalgebraic derivations in logic programming
- Coalgebraic semantics for parallel derivation strategies in logic programming
- Coalgebraic semantics for derivations in logic programming
- scientific article; zbMATH DE number 4181320 (Why is no real title available?)
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
- Universal constructions for (co)relations: categories, monoidal categories, and props
- Productive corecursion in logic programming
- Coalgebraic semantics for probabilistic logic programming
- Flexible coinductive logic programming
- Algebra and Coalgebra in Computer Science
- Category theoretic semantics for theorem proving in logic programming: embracing the laxness
- A type-theoretic approach to resolution
- scientific article; zbMATH DE number 7649893 (Why is no real title available?)
- Checked corecursive streams: expressivity and completeness
- Checking equivalence of corecursive streams: an inductive procedure
- Reductive logic, proof-search, and coalgebra: a perspective from resource semantics
- Reducing higher-order recursion scheme equivalence to coinductive higher-order constrained Horn clauses
This page was built for publication: Coalgebraic logic programming: from Semantics to Implementation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5739982)
