Proof-theoretic analysis of termination proofs

DOI10.1016/0168-0072(94)00056-9zbMath0844.03031OpenAlexW1968714331MaRDI QIDQ1899143

Wilfried Buchholz

Publication date: 27 August 1996

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

Full work available at URL: https://doi.org/10.1016/0168-0072(94)00056-9

zbMATH Keywords

rewrite systemorder typewell-foundednesslexicographic path orderingtermination orderinglengths of reduction sequencesmultiset path ordering

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Structure of proofs (03F07) Recursive ordinals and ordinal notations (03F15) Complexity of proofs (03F20)

Related Items (23)

How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study ⋮ Reverse mathematical bounds for the termination theorem ⋮ The proof-theoretic strength of Ramsey's theorem for pairs and two colors ⋮ Program Size Complexity of Correction Grammars in the Ershov Hierarchy ⋮ Investigations on slow versus fast growing: How to majorize slow growing functions nontrivially by fast growing ones ⋮ On the Computational Content of Termination Proofs ⋮ Unnamed Item ⋮ The Logic of Public Announcements, Common Knowledge, and Private Suspicions ⋮ Termination Proof of S-Expression Rewriting Systems with Recursive Path Relations ⋮ Unnamed Item ⋮ Some interesting connections between the slow growing hierarchy and the Ackermann function ⋮ Derivation lengths and order types of Knuth--Bendix orders ⋮ The Hydra battle and Cichon's principle ⋮ 2004 Summer Meeting of the Association for Symbolic Logic ⋮ Complexity Analysis by Rewriting ⋮ A lexicographic path order with slow growing derivation bounds ⋮ TERMINATION OF ABSTRACT REDUCTION SYSTEMS ⋮ Learning correction grammars ⋮ Lexicographic Path Induction ⋮ Dependent choice as a termination principle ⋮ Rice and Rice-Shapiro Theorems for transfinite correction grammars ⋮ Some results on cut-elimination, provable well-orderings, induction and reflection ⋮ Variations on a theme by Weiermann

Cites Work

• Unnamed Item
• Unnamed Item
• Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths
• A slow growing analogue to Buchholz' proof
• Termination proofs by multiset path orderings imply primitive recursive derivation lengths

This page was built for publication: Proof-theoretic analysis of termination proofs