Focussing and proof construction

DOI10.1016/S0168-0072(00)00032-4zbMath0966.03053MaRDI QIDQ1840461

Jean-Marc Andreoli

Publication date: 24 July 2001

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

zbMATH Keywords

linear logicconstraint propagationtableau methodsfocusing proofsproof construction

Mathematics Subject Classification ID

Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Logic programming (68N17) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items (23)

From axioms to synthetic inference rules via focusing ⋮ Structure of proofs and the complexity of cut elimination ⋮ MELL in the calculus of structures ⋮ Syntactic Completeness of Proper Display Calculi ⋮ A Categorical Setting for Lower Complexity ⋮ A categorical semantics for polarized MALL ⋮ Safe recursion revisited. I: Categorical semantics for lower complexity ⋮ Imperative programs as proofs via game semantics ⋮ Structural Focalization ⋮ An approach to innocent strategies as graphs ⋮ Strong and Weak Quantifiers in Focused NL$$_{\text {CL}}$$ ⋮ A logical characterization of forward and backward chaining in the inverse method ⋮ Multi-focused proofs with different polarity assignments ⋮ On the unity of duality ⋮ Modularity of proof-nets. Generating the type of a module. ⋮ Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method ⋮ Non-commutative proof construction: a constraint-based approach ⋮ On geometry of interaction for polarized linear logic ⋮ Axiom Directed Focusing ⋮ On linear logic planning and concurrency ⋮ Non decomposable connectives of linear logic ⋮ Rewritings for Polarized Multiplicative and Exponential Proof Structures ⋮ Connecting Sequent Calculi with Lorenzen-Style Dialogue Games

Uses Software

• Lolli

Cites Work

• Linear logic
• Light linear logic
• Logic programming in a fragment of intuitionistic linear logic
• Uniform proofs as a foundation for logic programming
• Logic Programming with Focusing Proofs in Linear Logic
• True concurrency semantics for a linear logic programming language with broadcast communication
• Resource-distribution via Boolean constraints

This page was built for publication: Focussing and proof construction