Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic

DOI10.1016/S0304-3975(99)00058-4zbMath0951.03058OpenAlexW2024442214MaRDI QIDQ1575865

Mitsuhiro Okada

Publication date: 23 August 2000

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(99)00058-4

zbMATH Keywords

phase semanticscut-eliminationfirst-order linear logichigher-order linear logicproof-normalization

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Related Items (22)

A completeness theorem for symmetric product phase spaces ⋮ Phase semantics and decidability of elementary affine logic ⋮ Phase semantics for light linear logic ⋮ Algebraic proof theory for substructural logics: cut-elimination and completions ⋮ On the Logic of Expansion in Natural Language ⋮ Maximally multi-focused proofs for skew non-commutative \texttt{MILL} ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms ⋮ On phase semantics and denotational semantics in multiplicative-additive linear logic ⋮ Orthogonality and Boolean Algebras for Deduction Modulo ⋮ A diagrammatic inference system with Euler circles ⋮ A phase semantics for polarized linear logic and second order conservativity ⋮ Algebraic proof theory: hypersequents and hypercompletions ⋮ MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics ⋮ Hyper-MacNeille completions of Heyting algebras ⋮ Towards a theory of resource: an approach based on soft exponentials ⋮ Unnamed Item ⋮ Strong normalization property for second order linear logic ⋮ Quantitative classical realizability ⋮ A uniform semantic proof for cut-elimination and completeness of various first and higher order logics. ⋮ Gentzen-type methods for bilattice negation ⋮ Towards a semantic characterization of cut-elimination

This page was built for publication: Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic