An Efficient Nominal Unification Algorithm

DOI10.4230/LIPIcs.RTA.2010.209zbMath1236.68138OpenAlexW1805897518MaRDI QIDQ5389146

Mateu Villaret, Jordi Levy

Publication date: 25 April 2012

Full work available at URL: http://subs.emis.de/LIPIcs/frontdoor_0682.html

zbMATH Keywords

unificationnominal logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Related Items (16)

Nominal unification with atom-variables ⋮ Unnamed Item ⋮ Nominal Unification and Matching of Higher Order Expressions with Recursive Let ⋮ Nominal syntax with atom substitutions ⋮ A Certified Functional Nominal C-Unification Algorithm ⋮ Unnamed Item ⋮ αCheck: A mechanized metatheory model checker ⋮ Nominal AC-matching ⋮ Unity in nominal equational reasoning: the algebra of equality on nominal sets ⋮ Rewriting with generalized nominal unification ⋮ Nominal equational problems ⋮ The First-Order Nominal Link ⋮ Completeness in PVS of a nominal unification algorithm ⋮ A formalisation of nominal C-matching through unification with protected variables ⋮ Formalising nominal C-unification generalised with protected variables ⋮ Nominal unification with letrec and environment-variables

This page was built for publication: An Efficient Nominal Unification Algorithm