A formal calculus for informal equality with binding

Murdoch Gabbay; Aad Mathijssen

A formal calculus for informal equality with binding

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

Abstract

In informal mathematical usage we often reason using languages with binding. We usually find ourselves placing capture-avoidance constraints on where variables can and cannot occur free. We describe a logical derivation system which allows a direct formalisation of such assertions, along with a direct formalisation of their constraints. We base our logic on equality, probably the simplest available judgement form. In spite of this, we can axiomatise systems of logic and computation such as first-order logic or the lambda-calculus in a very direct and natural way. We investigate the theory of derivations, prove a suitable semantics sound and complete, and discuss existing and future research. © Springer-Verlag Berlin Heidelberg 2007.

Original language	English
Title of host publication	Logic, Language, Information and Computation - 14th International Workshop, WoLLIC 2007, Proceedings
Pages	162-176
Number of pages	15
Volume	4576 LNCS
Publication status	Published - 2007
Event	14th International Workshop on Logic, Language, Information and Computation - Rio de Janeiro, Brazil Duration: 2 Jul 2007 → 5 Jul 2007

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	4576 LNCS
ISSN (Print)	0302-9743

Conference

Conference	14th International Workshop on Logic, Language, Information and Computation
Abbreviated title	WoLLIC
Country/Territory	Brazil
City	Rio de Janeiro
Period	2/07/07 → 5/07/07

Cite this

Gabbay, M., & Mathijssen, A. (2007). A formal calculus for informal equality with binding. In Logic, Language, Information and Computation - 14th International Workshop, WoLLIC 2007, Proceedings (Vol. 4576 LNCS, pp. 162-176). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4576 LNCS).

@inproceedings{222fdf570e694584a070d55f3bcc9c27,

title = "A formal calculus for informal equality with binding",

abstract = "In informal mathematical usage we often reason using languages with binding. We usually find ourselves placing capture-avoidance constraints on where variables can and cannot occur free. We describe a logical derivation system which allows a direct formalisation of such assertions, along with a direct formalisation of their constraints. We base our logic on equality, probably the simplest available judgement form. In spite of this, we can axiomatise systems of logic and computation such as first-order logic or the lambda-calculus in a very direct and natural way. We investigate the theory of derivations, prove a suitable semantics sound and complete, and discuss existing and future research. {\textcopyright} Springer-Verlag Berlin Heidelberg 2007.",

author = "Murdoch Gabbay and Aad Mathijssen",

year = "2007",

language = "English",

isbn = "9783540734437",

volume = "4576 LNCS",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "162--176",

booktitle = "Logic, Language, Information and Computation - 14th International Workshop, WoLLIC 2007, Proceedings",

note = "14th International Workshop on Logic, Language, Information and Computation, WoLLIC ; Conference date: 02-07-2007 Through 05-07-2007",

}

Gabbay, M & Mathijssen, A 2007, A formal calculus for informal equality with binding. in Logic, Language, Information and Computation - 14th International Workshop, WoLLIC 2007, Proceedings. vol. 4576 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4576 LNCS, pp. 162-176, 14th International Workshop on Logic, Language, Information and Computation, Rio de Janeiro, Brazil, 2/07/07.

A formal calculus for informal equality with binding. / Gabbay, Murdoch; Mathijssen, Aad.
Logic, Language, Information and Computation - 14th International Workshop, WoLLIC 2007, Proceedings. Vol. 4576 LNCS 2007. p. 162-176 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4576 LNCS).

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

TY - GEN

T1 - A formal calculus for informal equality with binding

AU - Gabbay, Murdoch

AU - Mathijssen, Aad

PY - 2007

Y1 - 2007

N2 - In informal mathematical usage we often reason using languages with binding. We usually find ourselves placing capture-avoidance constraints on where variables can and cannot occur free. We describe a logical derivation system which allows a direct formalisation of such assertions, along with a direct formalisation of their constraints. We base our logic on equality, probably the simplest available judgement form. In spite of this, we can axiomatise systems of logic and computation such as first-order logic or the lambda-calculus in a very direct and natural way. We investigate the theory of derivations, prove a suitable semantics sound and complete, and discuss existing and future research. © Springer-Verlag Berlin Heidelberg 2007.

AB - In informal mathematical usage we often reason using languages with binding. We usually find ourselves placing capture-avoidance constraints on where variables can and cannot occur free. We describe a logical derivation system which allows a direct formalisation of such assertions, along with a direct formalisation of their constraints. We base our logic on equality, probably the simplest available judgement form. In spite of this, we can axiomatise systems of logic and computation such as first-order logic or the lambda-calculus in a very direct and natural way. We investigate the theory of derivations, prove a suitable semantics sound and complete, and discuss existing and future research. © Springer-Verlag Berlin Heidelberg 2007.

M3 - Conference contribution

SN - 9783540734437

VL - 4576 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 162

EP - 176

BT - Logic, Language, Information and Computation - 14th International Workshop, WoLLIC 2007, Proceedings

T2 - 14th International Workshop on Logic, Language, Information and Computation

Y2 - 2 July 2007 through 5 July 2007

ER -

A formal calculus for informal equality with binding

Abstract

Publication series

Conference

Fingerprint

Cite this