(Nominal) Unification by Recursive Descent with Triangular Substitutions
Kumar, Ramana;
Norrish, Michael
2010-07-11
Conference Material
International Conference on Interactive Theorem Proving
Edinburgh, United Kingdom
51-66
We mechanise termination and correctness for two unification algorithms, written in a recursive descent style. One computes unifiers for first order terms, the other for nominal terms (terms including alpha-equivalent binding structure). Both algorithms work with triangular substitutions in accumulator-passing style: taking a substitution as input, and returning an extension of that substitution on success.
http://www.floc-conference.org/ITP-home.html
nicta:3724
Kumar, Ramana; Norrish, Michael. (Nominal) Unification by Recursive Descent with Triangular Substitutions. In: International Conference on Interactive Theorem Proving; Edinburgh, United Kingdom. 2010-07-11. 51-66. http://hdl.handle.net/102.100.100/107393?index=1
Loading citation data...
Citation counts
(Requires subscription to view)