A Sequent Calculus for Nominal Logic

Murdoch Gabbay; James Cheney

doi:10.1109/LICS.2004.6

A Sequent Calculus for Nominal Logic

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

Abstract

Nominal logic is a theory of names and binding based on the primitive concepts of freshness and swapping, with a self-dual N- (or "new")-quantifier, originally presented as a Hilbert-style axiom system extending first-order logic. We present a sequent calculus for nominal logic called fresh logic, or FL, admitting cut-elimination. We use FL to provide a proof-theoretic foundation for nominal logic programming and show how to interpret FOλ∇, another logic with a self-dual quantifier, within FL.

Original language	English
Title of host publication	Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science
Place of Publication	Washington, DC, USA
Publisher	Institute of Electrical and Electronics Engineers
Pages	139-148
Number of pages	10
ISBN (Print)	0-7695-2192-4
DOIs	https://doi.org/10.1109/LICS.2004.6
Publication status	Published - 2004

Publication series

Name	LICS '04
Publisher	IEEE Computer Society

Access to Document

10.1109/LICS.2004.6

http://dx.doi.org/10.1109/LICS.2004.6

Cite this

@inproceedings{d0c9298d17dc44abba6c7bfa93941ea4,

title = "A Sequent Calculus for Nominal Logic",

abstract = "Nominal logic is a theory of names and binding based on the primitive concepts of freshness and swapping, with a self-dual N- (or {"}new{"})-quantifier, originally presented as a Hilbert-style axiom system extending first-order logic. We present a sequent calculus for nominal logic called fresh logic, or FL, admitting cut-elimination. We use FL to provide a proof-theoretic foundation for nominal logic programming and show how to interpret FOλ∇, another logic with a self-dual quantifier, within FL.",

author = "Murdoch Gabbay and James Cheney",

year = "2004",

doi = "10.1109/LICS.2004.6",

language = "English",

isbn = "0-7695-2192-4",

series = "LICS '04",

publisher = "Institute of Electrical and Electronics Engineers",

pages = "139--148",

booktitle = "Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science",

address = "United States",

}

TY - GEN

T1 - A Sequent Calculus for Nominal Logic

AU - Gabbay, Murdoch

AU - Cheney, James

PY - 2004

Y1 - 2004

N2 - Nominal logic is a theory of names and binding based on the primitive concepts of freshness and swapping, with a self-dual N- (or "new")-quantifier, originally presented as a Hilbert-style axiom system extending first-order logic. We present a sequent calculus for nominal logic called fresh logic, or FL, admitting cut-elimination. We use FL to provide a proof-theoretic foundation for nominal logic programming and show how to interpret FOλ∇, another logic with a self-dual quantifier, within FL.

AB - Nominal logic is a theory of names and binding based on the primitive concepts of freshness and swapping, with a self-dual N- (or "new")-quantifier, originally presented as a Hilbert-style axiom system extending first-order logic. We present a sequent calculus for nominal logic called fresh logic, or FL, admitting cut-elimination. We use FL to provide a proof-theoretic foundation for nominal logic programming and show how to interpret FOλ∇, another logic with a self-dual quantifier, within FL.

U2 - 10.1109/LICS.2004.6

DO - 10.1109/LICS.2004.6

M3 - Conference contribution

SN - 0-7695-2192-4

T3 - LICS '04

SP - 139

EP - 148

BT - Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science

PB - Institute of Electrical and Electronics Engineers

CY - Washington, DC, USA

ER -

A Sequent Calculus for Nominal Logic

Abstract

Publication series

Access to Document

Fingerprint

Cite this