Refinement of proof-theoretic analysis of the lpo due to Buchholz
Toshiyasu Arai
TL;DR
This paper refines the proof-theoretic analysis of the lexicographic path order (lpo), enhancing understanding of its logical foundations and applications in term rewriting systems.
Contribution
It provides a more precise proof-theoretic framework for analyzing the lpo, improving upon Buchholz's original approach.
Findings
Enhanced proof-theoretic analysis of lpo
Refined bounds for termination proofs
Improved understanding of lpo's logical strength
Abstract
We give a refinement of proof-theoretic analysis of the lpo (lexicographic path order) due to W. Buchholz. This note was written in Feb. 5, 2015 when G. Moser visited Japan.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems