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)

• On linear logic planning and concurrency
• Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method
• Rewritings for polarized multiplicative and exponential proof structures
• Syntactic Completeness of Proper Display Calculi
• Lambek-Grishin calculus: focusing, display and full polarization
• Non decomposable connectives of linear logic
• From axioms to synthetic inference rules via focusing
• An approach to innocent strategies as graphs
• On the unity of duality
• Modularity of proof-nets. Generating the type of a module.
• A logical characterization of forward and backward chaining in the inverse method
• MELL in the calculus of structures
• Non-commutative proof construction: a constraint-based approach
• Axiom Directed Focusing
• Focusing and Polarization in Intuitionistic Logic
• Focusing and polarization in linear, intuitionistic, and classical logics
• Imperative programs as proofs via game semantics
• Canonicity of proofs in constructive modal logic
• On geometry of interaction for polarized linear logic
• Structure of proofs and the complexity of cut elimination
• On the meaning of focalization
• A categorical setting for lower complexity
• scientific article; zbMATH DE number 2090322 (Why is no real title available?)
• Focused proof search for linear logic in the calculus of structures
• Multi-focused proofs with different polarity assignments
• Structural focalization
• Construction of retractile proof structures
• Logic Programming with Focusing Proofs in Linear Logic
• Strong and weak quantifiers in focused \({\text{NL}}_{\text{CL}}\)
• A categorical semantics for polarized MALL
• Connecting sequent calculi with Lorenzen-style dialogue games
• Safe recursion revisited. I: Categorical semantics for lower complexity

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)