Fresh logic: Proof-theory and semantics for FM and nominal techniques

DOI10.1016/j.jal.2005.10.012zbMath1124.03010OpenAlexW2092116738MaRDI QIDQ2372191

Murdoch James Gabbay

Publication date: 25 July 2007

Published in: Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jal.2005.10.012

zbMATH Keywords

first-order logicKripke semanticsnominal logicFraenkel-Mostowski techniques

Mathematics Subject Classification ID

Other nonclassical logic (03B60) Cut-elimination and normal-form theorems (03F05)

Related Items

Nominal abstraction, αCheck: A mechanized metatheory model checker, Foundations of Nominal Techniques: Logic and Semantics of Variables in Abstract Syntax, Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms, PNL to HOL: from the logic of nominal sets to the logic of higher-order functions, A Simple Nominal Type Theory, Nominal Equational Logic

Uses Software

• SLMC

Cites Work

• A new approach to abstract syntax with variable binding
• Kripke-style models for typed lambda calculus
• Harvey Friedman's research on the foundations of mathematics
• About \({|}/{|}\)-quantifiers
• \(\pi\)-calculus in (Co)inductive-type theory
• The foundation of a generic theorem prover
• Nominal logic, a first order theory of names and binding
• A spatial logic for concurrency. I
• The continuum and first-order intuitionistic logic
• A proof theory for generic judgments
• Computer Science Logic
• Consistency of the theory of contexts
• Endliche Gruppen I
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item