Reductive logic, proof-search, and coalgebra: a perspective from resource semantics
From MaRDI portal
Publication:6612799
DOI10.1007/978-3-031-24117-8_23MaRDI QIDQ6612799
Simon Docherty, Alexander V. Gheorghiu, David J. Pym
Publication date: 1 October 2024
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Linear logic
- Hypersequent calculi for intuitionistic logic with classical atoms
- Computational interpretations of linear logic
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- From IF to BI. A tale of dependence and separation
- Don't eliminate cut
- Logic programming in a fragment of intuitionistic linear logic
- Isabelle. A generic theorem prover
- Un théorème sur les fonctions d'ensembles.
- Efficient resource management for linear logic proof search
- Edinburgh LCF. A mechanized logic of computation
- Possible worlds and resources: The semantics of \(\mathbf{BI}\)
- Full abstraction for PCF
- Nominal logic, a first order theory of names and binding
- Bunched logics displayed
- A stone-type duality theorem for separation logic via its underlying bunched logics
- Relating labelled and label-free bunched calculi in BI logic
- Focused proof-search in the logic of bunched implications
- The semantics and proof theory of the logic of bunched implications
- Linear resolution with selection function
- Uniform proofs as a foundation for logic programming
- A lattice-theoretical fixpoint theorem and its applications
- Focused and Synthetic Nested Sequents
- Programming with Higher-Order Logic
- Coalgebraic Semantics for Parallel Derivation Strategies in Logic Programming
- Coalgebraic Semantics for Derivations in Logic Programming
- The semantics of BI and resource tableaux
- Incorporating Tables into Proofs
- Coinductive Logic Programming and Its Applications
- The use of machines to assist in rigorous proof
- Contributions to the Theory of Logic Programming
- Logic Programming with Focusing Proofs in Linear Logic
- Algorithm = logic + control
- The Logic of Bunched Implications
- A Uniform Proof-theoretic Investigation of Linear Logic Programming
- Compositional semantics for a language of imperfect information
- A logical analysis of modules in logic programming
- Hyperclassical Logic (A.K.A. IF Logic) and Its Implications for Logical Theory
- BI as an assertion language for mutable data structures
- Resource-distribution via Boolean constraints
- Bialgebraic Semantics for Logic Programming
- Resource-distribution via Boolean constraints
- Sub-classical Boolean Bunched Logics and the Meaning of Par
- Co-Logic Programming: Extending Logic Programming with Coinduction
- Logic for Programming, Artificial Intelligence, and Reasoning
- The formal strong completeness of partial monoidal Boolean BI
- Coalgebraic logic programming: from Semantics to Implementation
This page was built for publication: Reductive logic, proof-search, and coalgebra: a perspective from resource semantics
