Focussing and proof construction
From MaRDI portal
Publication:1840461
DOI10.1016/S0168-0072(00)00032-4zbMATH Open0966.03053MaRDI QIDQ1840461FDOQ1840461
Authors: Jean-Marc Andreoli 
Publication date: 24 July 2001
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Recommendations
Proof theory in general (including proof-theoretic semantics) (03F03) Logic programming (68N17) Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Proof-theoretic aspects of linear logic and other substructural logics (03F52)
Cites Work
- Resource-distribution via Boolean constraints
- Linear logic
- Light linear logic
- Logic programming in a fragment of intuitionistic linear logic
- Logic Programming with Focusing Proofs in Linear Logic
- Uniform proofs as a foundation for logic programming
- True concurrency semantics for a linear logic programming language with broadcast communication
Cited In (32)
- From axioms to synthetic inference rules via focusing
- On geometry of interaction for polarized linear logic
- A categorical semantics for polarized MALL
- Non decomposable connectives of linear logic
- On the meaning of focalization
- Structural focalization
- Title not available (Why is that?)
- Syntactic Completeness of Proper Display Calculi
- Axiom Directed Focusing
- Safe recursion revisited. I: Categorical semantics for lower complexity
- An approach to innocent strategies as graphs
- Non-commutative proof construction: a constraint-based approach
- Multi-focused proofs with different polarity assignments
- A logical characterization of forward and backward chaining in the inverse method
- Strong and weak quantifiers in focused \({\text{NL}}_{\text{CL}}\)
- Focusing and Polarization in Intuitionistic Logic
- Focused proof search for linear logic in the calculus of structures
- Modularity of proof-nets. Generating the type of a module.
- Logic Programming with Focusing Proofs in Linear Logic
- Structure of proofs and the complexity of cut elimination
- Lambek-Grishin calculus: focusing, display and full polarization
- A categorical setting for lower complexity
- Connecting sequent calculi with Lorenzen-style dialogue games
- On linear logic planning and concurrency
- Focusing and polarization in linear, intuitionistic, and classical logics
- Construction of retractile proof structures
- Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method
- MELL in the calculus of structures
- On the unity of duality
- Canonicity of proofs in constructive modal logic
- Rewritings for polarized multiplicative and exponential proof structures
- Imperative programs as proofs via game semantics
Uses Software
This page was built for publication: Focussing and proof construction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1840461)
