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

DOI10.1016/J.JAL.2005.10.012MaRDI QIDQ2372191zbMATH OpenOpenAlexFDO

Authors Murdoch J. 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 logicnominal logicKripke semanticsFraenkel-Mostowski techniques

Mathematics Subject Classification ID

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

Recommendations

• A simple sequent calculus for nominal logic
• Foundations of Software Science and Computational Structures
• Nominal logic, a first order theory of names and binding
• scientific article; zbMATH DE number 2242589
• Nominal equational logic

Cites work

• scientific article; zbMATH DE number 3485758 (Why is no real title available?)
• scientific article; zbMATH DE number 3559512 (Why is no real title available?)
• scientific article; zbMATH DE number 482822 (Why is no real title available?)
• scientific article; zbMATH DE number 592370 (Why is no real title available?)
• scientific article; zbMATH DE number 1927564 (Why is no real title available?)
• scientific article; zbMATH DE number 1754648 (Why is no real title available?)
• scientific article; zbMATH DE number 2154399 (Why is no real title available?)
• scientific article; zbMATH DE number 874294 (Why is no real title available?)
• scientific article; zbMATH DE number 2242589 (Why is no real title available?)
• A new approach to abstract syntax with variable binding
• A proof theory for generic judgments
• A spatial logic for concurrency. I
• About \({|}/{|}\)-quantifiers
• Computer Science Logic
• Consistency of the theory of contexts
• Endliche Gruppen I
• Harvey Friedman's research on the foundations of mathematics
• Kripke-style models for typed lambda calculus
• Nominal logic, a first order theory of names and binding
• The continuum and first-order intuitionistic logic
• The foundation of a generic theorem prover
• -calculus in (Co)inductive-type theory

Cited in

(19)

• About \({|}/{|}\)-quantifiers
• scientific article; zbMATH DE number 4029553 (Why is no real title available?)
• A semantics for nabla
• PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
• Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
• Nominal abstraction
• Foundations of nominal techniques: logic and semantics of variables in abstract syntax
• Nominal logic, a first order theory of names and binding
• scientific article; zbMATH DE number 2242589 (Why is no real title available?)
• Completeness and Herbrand theorems for nominal logic
• On a monadic semantics for freshness
• A simple sequent calculus for nominal logic
• A simple nominal type theory
• αCheck: A mechanized metatheory model checker
• Nominal equational logic
• scientific article; zbMATH DE number 1980922 (Why is no real title available?)
• Foundations of Software Science and Computational Structures
• Equivariant ZFA and the foundations of nominal techniques
• Modelling generic judgements

Describes a project that uses

Uses Software

• SLMC

This page was built for publication: Fresh logic: Proof-theory and semantics for FM and nominal techniques

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2372191)