(Nominal) unification by recursive descent with triangular substitutions

DOI10.1007/978-3-642-14052-5_6zbMATH Open1291.68356OpenAlexW1512655913MaRDI QIDQ5747641FDOQ5747641

Authors: 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

Recommendations

• Nominal unification
• First-order unification by structural recursion
• Computer Science Logic
• A polynomial nominal unification algorithm
• Nominal unification of higher order expressions with recursive let

Mathematics Subject Classification ID

Cited In (9)

• First-order unification by structural recursion
• Alpha equivalence equalities
• A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols
• Completeness in PVS of a nominal unification algorithm
• Nominal essential intersection types
• A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
• Nominal syntax with atom substitutions
• A certified functional nominal C-unification algorithm
• Nominal AC-matching

Uses Software

• HOL

This page was built for publication: (Nominal) unification by recursive descent with triangular substitutions

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