Strong normalization for all-style LK^tq

DOI10.1007/3-540-61208-4_15MaRDI QIDQ4645240zbMATH OpenOpenAlexFDO

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

Publication date 10 January 2019

Published in Theorem Proving with Analytic Tableaux and Related Methods (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-61208-4_15

zbMATH Keywords

linear logiclogical reductionlogical rulesequent calculusstructural rule

Mathematics Subject Classification ID

Classical first-order logic (03B10) Subsystems of classical logic (including intuitionistic logic) (03B20) Cut-elimination and normal-form theorems (03F05)

Recommendations

• SN and CR for free-style LK^tq: linear decorations and simulation of normalization
• A short proof of the strong normalization of classical natural deduction with disjunction
• A strong normalization result for classical logic
• scientific article; zbMATH DE number 1499092
• A semantical proof of the strong normalization theorem for full propositional classical natural deduction

Cites work

• A new deconstructive logic: linear logic
• scientific article; zbMATH DE number 1337625 (Why is no real title available?)
• scientific article; zbMATH DE number 517072 (Why is no real title available?)
• scientific article; zbMATH DE number 786494 (Why is no real title available?)
• Linear logic
• Logic Programming with Focusing Proofs in Linear Logic
• Proof strategies in linear logic

Cited in

(4)

• Strong and weak quantifiers in focused \({\text{NL}}_{\text{CL}}\)
• Reduction in first-order logic compared with reduction in implicational logic
• SN and CR for free-style LK^tq: linear decorations and simulation of normalization
• Asymptotically almost all \lambda-terms are strongly normalizing

This page was built for publication: Strong normalization for all-style \(\mathbf{LK}^\mathrm{tq}\)

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