Equivariant unification

DOI10.1007/s10817-009-9164-3zbMath1207.68368OpenAlexW2914480101MaRDI QIDQ616849

James Cheney

Publication date: 12 January 2011

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-009-9164-3

zbMATH Keywords

equivariancenominal logicnominal unificationswapping-free

Mathematics Subject Classification ID

Related Items (11)

Nominal unification with atom-variables ⋮ Unnamed Item ⋮ Nominal Unification and Matching of Higher Order Expressions with Recursive Let ⋮ Nominal abstraction ⋮ Unnamed Item ⋮ αCheck: A mechanized metatheory model checker ⋮ On solving nominal disunification constraints ⋮ Fixed-Point Constraints for Nominal Equational Unification ⋮ Rewriting with generalized nominal unification ⋮ Nominal Confluence Tool ⋮ Contextual equivalence for inductive definitions with binders in higher order typed functional programming

Uses Software

• Nominal Isabelle

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A new approach to abstract syntax with variable binding
• Elements of finite model theory.
• Nominal techniques in Isabelle/HOL
• A polynomial nominal unification algorithm
• A proof theory for general unification
• The complexity of solving equations over finite groups
• Nominal unification
• Inapproximability results for equations over finite groups
• Nominal logic, a first order theory of names and binding
• Nominal rewriting
• Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming
• Nominal (Universal) Algebra: Equational Logic with Names and Binding
• Logic Programming
• Automata, Languages and Programming
• Completeness and Herbrand theorems for nominal logic
• Term Rewriting and Applications
• Typed Lambda Calculi and Applications
• Nominal Unification from a Higher-Order Perspective

This page was built for publication: Equivariant unification