A lexicographic path order with slow growing derivation bounds

Mathematical Logic Quarterly 55 (2):212-224 (2009)
  Copy   BIBTEX

Abstract

This paper is concerned with implicit computational complexity of the exptime computable functions. Modifying the lexicographic path order, we introduce a path order EPO. It is shown that a termination proof for a term rewriting system via EPO implies an exponential bound on the lengths of derivations. The path order EPO is designed so that every exptime function is representable as a term rewrite system compatible with EPO (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)

Categories

Keywords

Reprint years

DOI

10.1002/malq.200710090

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,423

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Lecture notes on term rewriting and computational complexity.Harvey Friedman - manuscript
Bounding derivation lengths with functions from the slow growing hierarchy.Andreas Weiermann - 1998 - Archive for Mathematical Logic 37 (5-6):427-441.
A general theorem on termination of rewriting.Jeremy E. Dawson - unknown
How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study.Andreas Weiermann - 1998 - Journal of Symbolic Logic 63 (4):1348-1370.
Investigations on slow versus fast growing: How to majorize slow growing functions nontrivially by fast growing ones. [REVIEW]Andreas Weiermann - 1995 - Archive for Mathematical Logic 34 (5):313-330.
The complexity of propositional proofs.Nathan Segerlind - 2007 - Bulletin of Symbolic Logic 13 (4):417-481.
Termination and confluence in infinitary term rewriting.P. H. Rodenburg - 1998 - Journal of Symbolic Logic 63 (4):1286-1296.
Ramsey's Theorem for Pairs and Provably Recursive Functions.Alexander Kreuzer & Ulrich Kohlenbach - 2009 - Notre Dame Journal of Formal Logic 50 (4):427-444.
Completeness of MLL Proof-Nets w.r.t. Weak Distributivity.Jean-Baptiste Joinet - 2007 - Journal of Symbolic Logic 72 (1):159 - 170.
Quantified propositional calculus and a second-order theory for NC1.Stephen Cook & Tsuyoshi Morioka - 2005 - Archive for Mathematical Logic 44 (6):711-749.
Proof complexity of propositional default logic.Olaf Beyersdorff, Arne Meier, Sebastian Müller, Michael Thomas & Heribert Vollmer - 2011 - Archive for Mathematical Logic 50 (7-8):727-742.
Complexity analysis of term rewriting systems.Stéphane Kaplan & Michèle Soria - forthcoming - Complexity.
Sharpened lower bounds for cut elimination.Samuel R. Buss - 2012 - Journal of Symbolic Logic 77 (2):656-668.
Proof Systems for Planning Under Cautious Semantics.Yuping Shen & Xishun Zhao - 2013 - Minds and Machines 23 (1):5-45.

Analytics

Added to PP
2014-01-16

Downloads
15 (#926,042)

6 months
1 (#1,516,429)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Proof-theoretic analysis of termination proofs.Wilfried Buchholz - 1995 - Annals of Pure and Applied Logic 75 (1-2):57-65.

Add more references