Church-Rosser property of a simple reduction for full first-order classical natural deduction

DOI10.1016/S0168-0072(02)00051-9zbMath1016.03006MaRDI QIDQ1861541

Y. Andou

Publication date: 9 March 2003

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

zbMATH Keywords

Church-Rosser propertyparallel reductionclassical natural deduction

Mathematics Subject Classification ID

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

Related Items (11)

A semantical proof of the strong normalization theorem for full propositional classical natural deduction ⋮ Unnamed Item ⋮ Some properties of the -calculus ⋮ Domain-Freeλµ-Calculus ⋮ Compositional Z: confluence proofs for permutative conversion ⋮ A short proof of the strong normalization of classical natural deduction with disjunction ⋮ Strong normalization of classical natural deduction with disjunctions ⋮ Non-strictly positive fixed points for classical natural deduction ⋮ 2003 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquim '03 ⋮ Church-Rosser property of a simple reduction for full first-order classical natural deduction ⋮ Z property for the shuffling calculus

Cites Work

• Untersuchungen über das logische Schliessen. I
• Church-Rosser property of a simple reduction for full first-order classical natural deduction
• A normalization-procedure for the first order classical natural deduction with full logical symbols
• Proofs of strong normalisation for second order classical natural deduction
• Parallel reductions in \(\lambda\)-calculus
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Church-Rosser property of a simple reduction for full first-order classical natural deduction