Dependent choice as a termination principle

Archive for Mathematical Logic 59 (3-4):503-516 (2020)
  Copy   BIBTEX

Abstract

We introduce a new formulation of the axiom of dependent choice, which can be viewed as an abstract termination principle that in particular generalises recursive path orderings, the latter being fundamental tools used to establish termination of rewrite systems. We consider several variants of our termination principle, and relate them to general termination theorems in the literature.

Categories

Add categories

Keywords

Reprint years

DOI

10.1007/s00153-019-00706-6

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 101,297

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

A general theorem on termination of rewriting.Jeremy E. Dawson - unknown
Simply terminating rewrite systems with long derivations.Ingo Lepper - 2004 - Archive for Mathematical Logic 43 (1):1-18.
Extensions of arithmetic for proving termination of computations.Clement F. Kent & Bernard R. Hodgson - 1989 - Journal of Symbolic Logic 54 (3):779-794.
Strong termination for the epsilon substitution method.Grigori Mints - 1996 - Journal of Symbolic Logic 61 (4):1193-1205.
Modular termination of basic narrowing and equational unification.María Alpuente, Santiago Escobar & José Iborra - 2011 - Logic Journal of the IGPL 19 (6):731-762.
Bounding derivation lengths with functions from the slow growing hierarchy.Andreas Weiermann - 1998 - Archive for Mathematical Logic 37 (5-6):427-441.
On the termination of russell’s description elimination algorithm.Clemens Grabmayer, Joop Leo, Vincent van Oostrom & Albert Visser - 2011 - Review of Symbolic Logic 4 (3):367-393.
A lexicographic path order with slow growing derivation bounds.Naohi Eguchi - 2009 - Mathematical Logic Quarterly 55 (2):212-224.
Termination Proofs for Logic Programs.Lutz Plümer - 1990 - Springer.

Analytics

Added to PP
2020-01-16

Downloads
14 (#1,283,901)

6 months
4 (#1,263,115)

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.
The equivalence of bar recursion and open recursion.Thomas Powell - 2014 - Annals of Pure and Applied Logic 165 (11):1727-1754.

Add more references