The language of Stratified Sets is confluent and strongly normalising

Research output: Contribution to journalArticle

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 languageEnglish
Article number12
JournalLogical Methods in Computer Science
Volume14
Issue number2
DOIs
Publication statusPublished - 22 May 2018

Fingerprint

Stratification
Strong Normalization
Confluence
First-order Logic
Categorical or nominal
Substitution
Imply
Algebra
Language

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 = "5",
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",

}

The language of Stratified Sets is confluent and strongly normalising. / Gabbay, Murdoch J.

In: Logical Methods in Computer Science, Vol. 14, No. 2, 12, 22.05.2018.

Research output: Contribution to journalArticle

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

VL - 14

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 2

M1 - 12

ER -