scientific article; zbMATH DE number 1302675

MaRDI QIDQ4249227zbMATH OpenFDO

Authors Elias Tahhan-Bittar

Publication date 8 October 2000

Full work available at URL https://eudml.org/doc/208921

zbMATH Keywords

cut eliminationstrong normalizationterm rewriting systems

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

Review text

\textit{A. G. Dragalin} [Mathematical intuitionism (American Mathematical Society, Providence) (1988; Zbl 0634.03054); translation from the Russian original (Nauka, Moskva) (1979; Zbl 0439.03041)] gave a strong normalization proof for sequent L-systems when two cuts are never permuted. One of the proofs in the paper under review can be seen as a version of Dragalin's proof for a more complicated but more uniform notation for derivations. The only information given for an inference rule in this notation is the number of premises and whether the rule is active or passive with respect to the cut. Another proof uses results from the theory of term rewriting systems. For the entire collection see [Zbl 0913.00019].

Recommendations

• Strong normalisation of cut-elimination in classical logic
• Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions
• Strong normalisation for a Gentzen-like cut-elimination procedure
• scientific article; zbMATH DE number 874672

Cited in

(7)

• Some general results about proof normalization
• Gentzen's second consistency proof and strong cut-elimination
• Strong normalisation for a Gentzen-like cut-elimination procedure
• Lexicographic Path Induction
• Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus
• A short proof of the strong normalization of classical natural deduction with disjunction
• scientific article; zbMATH DE number 966897 (Why is no real title available?)

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 Q4249227)