Structural focalization

DOI10.1145/2629678MaRDI QIDQ2946730zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Robert J. Simmons

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1109.6273

zbMATH Keywords

cut admissibilityfocusingidentity expansionintuitionstic logicnormalizationpolarized logicproof searchproof terms

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07)

Abstract: Focusing, introduced by Jean-Marc Andreoli in the context of classical linear logic, defines a normal form for sequent calculus derivations that cuts down on the number of possible derivations by eagerly applying invertible rules and grouping sequences of non-invertible rules. A focused sequent calculus is defined relative to some non-focused sequent calculus; focalization is the property that every non-focused derivation can be transformed into a focused derivation. In this paper, we present a focused sequent calculus for propositional intuitionistic logic and prove the focalization property relative to a standard presentation of propositional intuitionistic logic. Compared to existing approaches, the proof is quite concise, depending only on the internal soundness and completeness of the focused logic. In turn, both of these properties can be established (and mechanically verified) by structural induction in the style of Pfenning's structural cut elimination without the need for any tedious and repetitious invertibility lemmas. The proof of cut admissibility for the focused system, which establishes internal soundness, is not particularly novel. The proof of identity expansion, which establishes internal completeness, is a major contribution of this work.

Recommendations

• A semantical analysis of focusing and contraction in intuitionistic logic
• Focusing and Polarization in Intuitionistic Logic
• The focused calculus of structures
• Logical Approaches to Computational Barriers
• Focusing and polarization in linear, intuitionistic, and classical logics

Cites work

• A focused approach to combining logics
• A Linear Spine Calculus
• A logical characterization of forward and backward chaining in the inverse method
• Compact proof certificates for linear logic
• Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method
• Focused natural deduction
• Focusing and higher-order abstract syntax
• Focusing and polarization in linear, intuitionistic, and classical logics
• Focusing on pattern matching
• Focussing and proof construction
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 2079018 (Why is no real title available?)
• scientific article; zbMATH DE number 2120508 (Why is no real title available?)
• Locus solum: From the rules of logic to the logic of rules.
• Logic Programming with Focusing Proofs in Linear Logic
• Logical approximation for program analysis
• On the unity of duality
• On the unity of logic
• Practical foundations for programming languages
• Proof search in lax logic
• Structural cut elimination. I: Intuitionistic and classical logic
• Types for Proofs and Programs
• Uniform proofs as a foundation for logic programming
• Untersuchungen über das logische Schliessen. I

Cited in

(38)

• Focusing and polarization in linear, intuitionistic, and classical logics
• Non-commutative logic. III: Focusing proofs.
• Focal points in framed strategic forms
• Formalized meta-theory of sequent calculi for substructural logics
• The polarized \(\lambda\)-calculus
• From axioms to synthetic inference rules via focusing
• A formally verified cut-elimination procedure for linear nested sequents for tense logic
• The explosion calculus
• An exponential lower bound for proofs in focused calculi
• Mechanizing focused linear logic in Coq
• Formalized meta-theory of sequent calculi for linear logics
• Focused and Synthetic Nested Sequents
• The focused calculus of structures
• On the meaning of focalization
• From focalization of logic to the logic of focalization
• A semantical analysis of focusing and contraction in intuitionistic logic
• From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
• Focusing and Polarization in Intuitionistic Logic
• Focalisation and Classical Realisability
• A resource aware semantics for a focused intuitionistic calculus
• Multi-focused cut elimination
• Expressing additives using multiplicatives and subexponentials
• A systematic approach to canonicity in the classical sequent calculus
• Focused natural deduction
• Linking focusing and resolution with selection
• Undecidability of multiplicative subexponential logic
• Cut elimination in multifocused linear logic
• A focused linear logical framework and its application to metatheory of object logics
• Strong sums in focused logic
• Modular focused proof systems for intuitionistic modal logics
• Focusing in Orthologic
• Focusing Strategies in the Sequent Calculus of Synthetic Connectives
• A multi-focused proof system isomorphic to expansion proofs
• Logical Approaches to Computational Barriers
• Focused linear logic and the \(\lambda\)-calculus
• Focusing Gentzen's LK proof system
• Permutability in proof terms for intuitionistic sequent calculus with cuts
• Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic

Describes a project that uses

Uses Software

• Twelf

This page was built for publication: Structural focalization

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2946730)