(Nominal) Unification by Recursive Descent with Triangular Substitutions

Select |




Print


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



PermaLink

http://hdl.handle.net/102.100.100/107393?index=1

Loading citation data...

Citation counts
(Requires subscription to view)