(Nominal) Unification by Recursive Descent with Triangular Substitutions

DOI10.1007/978-3-642-14052-5_6zbMath1291.68356OpenAlexW1512655913MaRDI QIDQ5747641

Ramana Kumar, Michael Norrish

Publication date: 14 September 2010

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-14052-5_6

Mathematics Subject Classification ID

Related Items (8)

Nominal essential intersection types ⋮ Nominal syntax with atom substitutions ⋮ A Certified Functional Nominal C-Unification Algorithm ⋮ Nominal AC-matching ⋮ A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols ⋮ Alpha equivalence equalities ⋮ Completeness in PVS of a nominal unification algorithm ⋮ A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols

Uses Software

• HOL

This page was built for publication: (Nominal) Unification by Recursive Descent with Triangular Substitutions