Completeness and Herbrand theorems for nominal logic

DOI10.2178/jsl/1140641176zbMath1100.03016OpenAlexW2161033077MaRDI QIDQ5477637

James Cheney

Publication date: 5 July 2006

Full work available at URL: https://doi.org/10.2178/jsl/1140641176

zbMATH Keywords

equivarianceabstract syntax treesname-swappingfresh name generationfinite-support modelsgeneralization of Herbrand modelsideal-supported modelsNominal logicnominal-universal theories

Mathematics Subject Classification ID

Other nonclassical logic (03B60) Logic in computer science (03B70)

Related Items

Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free, Equivariant unification, αCheck: A mechanized metatheory model checker, Foundations of Nominal Techniques: Logic and Semantics of Variables in Abstract Syntax, PNL to HOL: from the logic of nominal sets to the logic of higher-order functions, A Simple Nominal Type Theory, Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables, Term-generic logic, Nominal Equational Logic

Cites Work

• An attack on the Needham-Schroeder public-key authentication protocol
• A new approach to abstract syntax with variable binding
• A calculus of mobile processes. I
• Infinitary lambda calculus
• Orienting rewrite rules with the Knuth-Bendix order.
• A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
• A framework for defining logics
• Using encryption for authentication in large networks of computers
• The Logic of Bunched Implications
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item