(Nominal) unification by recursive descent with triangular substitutions

DOI10.1007/978-3-642-14052-5_6MaRDI QIDQ5747641zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

Cited in

(11)

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

Describes a project that uses

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)