Fresh Logic: proof-theory and semantics for FM and nominal techniques |
| |
| Authors: | Murdoch J Gabbay |
| |
| Institution: | aDepartment of Computer Science, King's College, London, UK |
| |
| Abstract: | In this paper we introduce Fresh Logic, a natural deduction style first-order logic extended with term-formers and quantifiers derived from the FM-sets model of names and binding in abstract syntax. Fresh Logic can be classical or intuitionistic depending on whether we include a law of excluded middle; we present a proof-normalisation procedure for the intuitionistic case and a semantics based on Kripke models in FM-sets for which it is sound and complete. |
| |
| Keywords: | Nominal logic First-order logic Semantics of intuitionistic logic Kripke semantics Freshness Nominal sets Fraenkel– Mostowski techniques |
| 本文献已被 ScienceDirect 等数据库收录！ |
