Dependent choice as a termination principle

Thomas Powell

doi:10.1007/s00153-019-00706-6

Dependent choice as a termination principle

Thomas Powell

Technische Universität Darmstadt

Research output: Contribution to journal › Article › peer-review

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.

Original language	English
Pages (from-to)	503-516
Number of pages	14
Journal	Archive for Mathematical Logic
Volume	59
Issue number	3-4
Early online date	16 Jan 2020
DOIs	https://doi.org/10.1007/s00153-019-00706-6
Publication status	Published - 1 May 2020

Keywords

Arithmetic in all finite types
Dependent choice
Higher order reverse mathematics
Path orderings
Termination

ASJC Scopus subject areas

Philosophy
Logic

Access to Document

10.1007/s00153-019-00706-6

Cite this

@article{5bc9b2ab12bb4dd795604505244bc5ba,

title = "Dependent choice as a termination principle",

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.",

keywords = "Arithmetic in all finite types, Dependent choice, Higher order reverse mathematics, Path orderings, Termination",

author = "Thomas Powell",

year = "2020",

month = may,

day = "1",

doi = "10.1007/s00153-019-00706-6",

language = "English",

volume = "59",

pages = "503--516",

journal = "Archive for Mathematical Logic",

issn = "0933-5846",

publisher = "Springer",

number = "3-4",

}

TY - JOUR

T1 - Dependent choice as a termination principle

AU - Powell, Thomas

PY - 2020/5/1

Y1 - 2020/5/1

N2 - 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.

AB - 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.

KW - Arithmetic in all finite types

KW - Dependent choice

KW - Higher order reverse mathematics

KW - Path orderings

KW - Termination

UR - http://www.scopus.com/inward/record.url?scp=85078608142&partnerID=8YFLogxK

U2 - 10.1007/s00153-019-00706-6

DO - 10.1007/s00153-019-00706-6

M3 - Article

SN - 0933-5846

VL - 59

SP - 503

EP - 516

JO - Archive for Mathematical Logic

JF - Archive for Mathematical Logic

IS - 3-4

ER -

Dependent choice as a termination principle

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this