Focussing and proof construction

DOI10.1016/S0168-0072(00)00032-4MaRDI QIDQ1840461zbMATH OpenFDO

Authors 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

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)

Recommendations

• Logic Programming with Focusing Proofs in Linear Logic
• From focalization of logic to the logic of focalization
• Focusing and polarization in linear, intuitionistic, and classical logics
• Focusing and Polarization in Intuitionistic Logic
• Non-commutative proof construction: a constraint-based approach

Cites work

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

Cited in

(32)

• From axioms to synthetic inference rules via focusing
• A categorical semantics for polarized MALL
• On geometry of interaction for polarized linear logic
• Non decomposable connectives of linear logic
• On the meaning of focalization
• Structural focalization
• scientific article; zbMATH DE number 2090322 (Why is no real title available?)
• Safe recursion revisited. I: Categorical semantics for lower complexity
• Syntactic Completeness of Proper Display Calculi
• Axiom Directed Focusing
• 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
• A categorical setting for lower complexity
• Lambek-Grishin calculus: focusing, display and full polarization
• 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
• Rewritings for polarized multiplicative and exponential proof structures
• Canonicity of proofs in constructive modal logic
• Imperative programs as proofs via game semantics

Describes a project that uses

Uses Software

• Lolli

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)