The language of Stratified Sets is confluent and strongly normalising

Murdoch J. Gabbay

doi:10.23638/LMCS-14(2:12)2018

The language of Stratified Sets is confluent and strongly normalising

Murdoch J. Gabbay

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

1 Citation (Scopus)

42 Downloads (Pure)

Abstract

We study the properties of the language of Stratified Sets (first-order logic with ∈ and a stratification condition) as used in TST, TZT, and (with stratifiability instead of stratification) in Quine's NF. We find that the syntax forms a nominal algebra for substitution and that stratification and stratifiability imply confluence and strong normalisation under rewrites corresponding naturally to β-conversion.

Original language	English
Article number	12
Journal	Logical Methods in Computer Science
Volume	14
Issue number	2
DOIs	https://doi.org/10.23638/LMCS-14(2:12)2018
Publication status	Published - 22 May 2018

Access to Document

10.23638/LMCS-14(2:12)2018Licence: CC BY

Download pdfFinal published version, 507 KBLicence: CC BY

Cite this

@article{a62f16dfb71e41e09371b0244678eeea,

title = "The language of Stratified Sets is confluent and strongly normalising",

abstract = "We study the properties of the language of Stratified Sets (first-order logic with ∈ and a stratification condition) as used in TST, TZT, and (with stratifiability instead of stratification) in Quine's NF. We find that the syntax forms a nominal algebra for substitution and that stratification and stratifiability imply confluence and strong normalisation under rewrites corresponding naturally to β-conversion. ",

author = "Gabbay, {Murdoch J.}",

year = "2018",

month = may,

day = "22",

doi = "10.23638/LMCS-14(2:12)2018",

language = "English",

volume = "14",

journal = "Logical Methods in Computer Science",

issn = "1860-5974",

publisher = "Technischen Universitat Braunschweig",

number = "2",

}

TY - JOUR

T1 - The language of Stratified Sets is confluent and strongly normalising

AU - Gabbay, Murdoch J.

PY - 2018/5/22

Y1 - 2018/5/22

N2 - We study the properties of the language of Stratified Sets (first-order logic with ∈ and a stratification condition) as used in TST, TZT, and (with stratifiability instead of stratification) in Quine's NF. We find that the syntax forms a nominal algebra for substitution and that stratification and stratifiability imply confluence and strong normalisation under rewrites corresponding naturally to β-conversion.

AB - We study the properties of the language of Stratified Sets (first-order logic with ∈ and a stratification condition) as used in TST, TZT, and (with stratifiability instead of stratification) in Quine's NF. We find that the syntax forms a nominal algebra for substitution and that stratification and stratifiability imply confluence and strong normalisation under rewrites corresponding naturally to β-conversion.

U2 - 10.23638/LMCS-14(2:12)2018

DO - 10.23638/LMCS-14(2:12)2018

M3 - Article

SN - 1860-5974

VL - 14

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

IS - 2

M1 - 12

ER -

The language of Stratified Sets is confluent and strongly normalising

Abstract

Access to Document

Fingerprint

Cite this