Proof-theoretic analysis of termination proofs
From MaRDI portal
Publication:1899143
DOI10.1016/0168-0072(94)00056-9zbMath0844.03031OpenAlexW1968714331MaRDI QIDQ1899143
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
rewrite systemorder typewell-foundednesslexicographic path orderingtermination orderinglengths of reduction sequencesmultiset path ordering
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
This page was built for publication: Proof-theoretic analysis of termination proofs