SN and CR for free-style LKtq: linear decorations and simulation of normalization

DOI10.2178/JSL/1190150036MaRDI QIDQ4532608zbMATH OpenOpenAlexFDO

Authors Jean-Baptiste Joinet, Harold Schellinx, Lorenzo Tortora de Falco

Publication date 29 October 2002

Published in Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2178/jsl/1190150036

zbMATH Keywords

classical logiclinear logicstrongly normalizing strategies for cut reductions

Mathematics Subject Classification ID

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

Recommendations

• Strong normalization for all-style \(\mathbf{LK}^\mathrm{tq}\)
• A strong normalization result for classical logic
• On the linear decoration of intuitionistic derivations
• Strong normalisation of cut-elimination in classical logic
• From propositional to linear logic: An introduction. Decoration, simulation, normalization

Cites work

• Linear logic
• Untersuchungen über das logische Schliessen. II

Cited in

(2)

• Strong normalization for all-style \(\mathbf{LK}^\mathrm{tq}\)
• Polarized and focalized linear and classical proofs

This page was built for publication: SN and CR for free-style LK^tq: linear decorations and simulation of normalization

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