Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations

DOI10.1016/j.jsc.2014.09.033zbMath1315.68168OpenAlexW2028930358MaRDI QIDQ485843

Sarah Winkler, Harald Zankl, Aart Middeldorp

Publication date: 14 January 2015

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jsc.2014.09.033

zbMATH Keywords

terminationterm rewritingautomationordinals

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Related Items (2)

On some slowly terminating term rewriting systems ⋮ Unnamed Item

Uses Software

• Tyrolean

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths
• The Hydra battle and Cichon's principle
• Mechanically proving termination using polynomial interpretations
• Ordinal arithmetic: Algorithms and mechanization
• Matrix interpretations for proving termination of term rewriting
• An independence result for \((\Pi^ 1_ 1-CA)+BI\)
• Testing positiveness of polynomials
• Termination of rewrite systems by elementary interpretations
• Simply terminating rewrite systems with long derivations
• Die another day
• Ordinals and Knuth-Bendix Orders
• Beyond Peano Arithmetic – Automatically Proving Termination of the Goodstein Sequence
• Satisfiability of Non-linear (Ir)rational Arithmetic
• The Hydra Battle Revisited
• SAT Solving for Termination Analysis with Polynomial Interpretations
• Accessible Independence Results for Peano Arithmetic
• A Relationship Among Gentzen's Proof-Reduction, Kirby-Paris' Hydra Game and Buchholz's Hydra Game
• A Short Proof of Two Recently Discovered Independence Results Using Recursion Theoretic Methods
• Trees, ordinals and termination
• Termination proofs and the length of derivations
• Automatic Proofs of Termination With Elementary Interpretations
• On Transfinite Knuth-Bendix Orders
• An Abstract Domain to Infer Ordinal-Valued Ranking Functions
• Artificial Intelligence and Symbolic Computation
• Termination Tools in Ordered Completion
• On the restricted ordinal theorem
• The Derivational Complexity Induced by the Dependency Pair Method
• The termination hierarchy for term rewriting
• Derivation lengths and order types of Knuth--Bendix orders

This page was built for publication: Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations