scientific article; zbMATH DE number 1231526

MaRDI QIDQ4222841zbMATH OpenFDO

Authors Mitsuhiro Okada

Publication date 14 December 1998

Full work available at URL http://www.elsevier.com/cas/tree/store/tcs/free/noncas/pc/volume3.htm#okada

zbMATH Keywords

cut-eliminationextension of Girard's phase semanticsphase semantics for proofsproof-normalization theorem

Mathematics Subject Classification ID

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

Recommendations

• Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic
• A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
• Completeness of second-order intuitionistic propositional logic with respect to phase semantics for proof-terms
• Completeness and cut-elimination theorems for high-order classical logic. Constructive method

Cited in

(8)

• Phase semantics for light linear logic
• Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic
• A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
• Completeness and cut-elimination theorems for high-order classical logic. Constructive method
• Completeness of second-order intuitionistic propositional logic with respect to phase semantics for proof-terms
• A phase semantics for polarized linear logic and second order conservativity
• Phase semantics and decidability of elementary affine logic
• Towards a semantic characterization of cut-elimination

This page was built for publication:

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