A normalization-procedure for the first order classical natural deduction with full logical symbols

DOI10.21099/tkbjm/1496162804zbMath0835.03021OpenAlexW1584940602MaRDI QIDQ1904467

Andou Yuuki

Publication date: 22 April 1996

Published in: Tsukuba Journal of Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.21099/tkbjm/1496162804

zbMATH Keywords

reductionnatural deductionnormalization procedureclassical first-order logic

Mathematics Subject Classification ID

Classical first-order logic (03B10) Cut-elimination and normal-form theorems (03F05)

Related Items (6)

Strong normalization of the second-order symmetric \(\lambda \mu\)-calculus ⋮ Some properties of the -calculus ⋮ Domain-Freeλµ-Calculus ⋮ Existential Type Systems with No Types in Terms ⋮ Single-assumption systems in proof-theoretic semantics ⋮ Church-Rosser property of a simple reduction for full first-order classical natural deduction

This page was built for publication: A normalization-procedure for the first order classical natural deduction with full logical symbols