A Simpler Proof Theory for Nominal Logic

James Cheney

doi:10.1007/978-3-540-31982-5_24

A Simpler Proof Theory for Nominal Logic

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

Nominal logic is a variant of first-order logic equipped with a “fresh-name quantifier” И and other features useful for reasoning about languages with bound names. Its original presentation was as a Hilbert axiomatic theory, but several attempts have been made to provide more convenient Gentzen-style sequent or natural deduction calculi for nominal logic. Unfortunately, the rules for И in these calculi involve complicated side-conditions, so using and proving properties of these calculi is difficult. This paper presents an improved sequent calculus NL ⇒ for nominal logic. Basic results such as cut-elimination and conservativity with respect to nominal logic are proved. Also, NL ⇒ is used to solve an open problem, namely relating nominal logic’s И-quantifier and the self-dual ∇-quantifier of Miller and Tiu’s FOλ∇

Original language	English
Title of host publication	Foundations of Software Science and Computational Structures
Subtitle of host publication	8th International Conference, FOSSACS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005. Proceedings
Editors	Vladimiro Sassone
Publisher	Springer Berlin Heidelberg
Pages	379-394
Number of pages	16
Volume	3441
ISBN (Electronic)	978-3-540-31982-5
ISBN (Print)	978-3-540-25388-4
DOIs	https://doi.org/10.1007/978-3-540-31982-5_24
Publication status	Published - 2005

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin Heidelberg
Volume	3441

Access to Document

10.1007/978-3-540-31982-5_24

http://dx.doi.org/10.1007/978-3-540-31982-5_24

Cite this

Cheney, J. (2005). A Simpler Proof Theory for Nominal Logic. In V. Sassone (Ed.), Foundations of Software Science and Computational Structures: 8th International Conference, FOSSACS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005. Proceedings (Vol. 3441, pp. 379-394). (Lecture Notes in Computer Science; Vol. 3441). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-540-31982-5_24

Cheney, James. / A Simpler Proof Theory for Nominal Logic. Foundations of Software Science and Computational Structures: 8th International Conference, FOSSACS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005. Proceedings. editor / Vladimiro Sassone. Vol. 3441 Springer Berlin Heidelberg, 2005. pp. 379-394 (Lecture Notes in Computer Science).

@inproceedings{5bfc9483852e4e129806f6e027321009,

title = "A Simpler Proof Theory for Nominal Logic",

abstract = "Nominal logic is a variant of first-order logic equipped with a “fresh-name quantifier” И and other features useful for reasoning about languages with bound names. Its original presentation was as a Hilbert axiomatic theory, but several attempts have been made to provide more convenient Gentzen-style sequent or natural deduction calculi for nominal logic. Unfortunately, the rules for И in these calculi involve complicated side-conditions, so using and proving properties of these calculi is difficult. This paper presents an improved sequent calculus NL ⇒ for nominal logic. Basic results such as cut-elimination and conservativity with respect to nominal logic are proved. Also, NL ⇒ is used to solve an open problem, namely relating nominal logic{\textquoteright}s И-quantifier and the self-dual ∇-quantifier of Miller and Tiu{\textquoteright}s FOλ∇",

author = "James Cheney",

year = "2005",

doi = "10.1007/978-3-540-31982-5_24",

language = "English",

isbn = "978-3-540-25388-4",

volume = "3441",

series = "Lecture Notes in Computer Science",

publisher = "Springer Berlin Heidelberg",

pages = "379--394",

editor = "Vladimiro Sassone",

booktitle = "Foundations of Software Science and Computational Structures",

}

Cheney, J 2005, A Simpler Proof Theory for Nominal Logic. in V Sassone (ed.), Foundations of Software Science and Computational Structures: 8th International Conference, FOSSACS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005. Proceedings. vol. 3441, Lecture Notes in Computer Science, vol. 3441, Springer Berlin Heidelberg, pp. 379-394. https://doi.org/10.1007/978-3-540-31982-5_24

A Simpler Proof Theory for Nominal Logic. / Cheney, James.

Foundations of Software Science and Computational Structures: 8th International Conference, FOSSACS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005. Proceedings. ed. / Vladimiro Sassone. Vol. 3441 Springer Berlin Heidelberg, 2005. p. 379-394 (Lecture Notes in Computer Science; Vol. 3441).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - A Simpler Proof Theory for Nominal Logic

AU - Cheney, James

PY - 2005

Y1 - 2005

N2 - Nominal logic is a variant of first-order logic equipped with a “fresh-name quantifier” И and other features useful for reasoning about languages with bound names. Its original presentation was as a Hilbert axiomatic theory, but several attempts have been made to provide more convenient Gentzen-style sequent or natural deduction calculi for nominal logic. Unfortunately, the rules for И in these calculi involve complicated side-conditions, so using and proving properties of these calculi is difficult. This paper presents an improved sequent calculus NL ⇒ for nominal logic. Basic results such as cut-elimination and conservativity with respect to nominal logic are proved. Also, NL ⇒ is used to solve an open problem, namely relating nominal logic’s И-quantifier and the self-dual ∇-quantifier of Miller and Tiu’s FOλ∇

AB - Nominal logic is a variant of first-order logic equipped with a “fresh-name quantifier” И and other features useful for reasoning about languages with bound names. Its original presentation was as a Hilbert axiomatic theory, but several attempts have been made to provide more convenient Gentzen-style sequent or natural deduction calculi for nominal logic. Unfortunately, the rules for И in these calculi involve complicated side-conditions, so using and proving properties of these calculi is difficult. This paper presents an improved sequent calculus NL ⇒ for nominal logic. Basic results such as cut-elimination and conservativity with respect to nominal logic are proved. Also, NL ⇒ is used to solve an open problem, namely relating nominal logic’s И-quantifier and the self-dual ∇-quantifier of Miller and Tiu’s FOλ∇

U2 - 10.1007/978-3-540-31982-5_24

DO - 10.1007/978-3-540-31982-5_24

M3 - Conference contribution

SN - 978-3-540-25388-4

VL - 3441

T3 - Lecture Notes in Computer Science

SP - 379

EP - 394

BT - Foundations of Software Science and Computational Structures

A2 - Sassone, Vladimiro

PB - Springer Berlin Heidelberg

ER -

Cheney J. A Simpler Proof Theory for Nominal Logic. In Sassone V, editor, Foundations of Software Science and Computational Structures: 8th International Conference, FOSSACS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005. Proceedings. Vol. 3441. Springer Berlin Heidelberg. 2005. p. 379-394. (Lecture Notes in Computer Science). doi: 10.1007/978-3-540-31982-5_24

A Simpler Proof Theory for Nominal Logic

Abstract

Publication series

Access to Document

Fingerprint

Cite this