Abstract
Higher-order unification is a method for unifying terms in the Simple Theory of Types [28], that is, given two typed lambda-terms e1 and e2, finding a substitution σ for the free variables of the two terms such that σ(e1) and σ(e2) are equivalent under the conversion rules of the calculus. As discussed above, this problem is fundamental to theorem proving in higher-order contexts (see Chapter §1 for references). In this chapter, we adapt the method of transformations to higher-order unification.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1991 Springer Science+Business Media New York
About this chapter
Cite this chapter
Snyder, W. (1991). Higher Order Unification. In: A Proof Theory for General Unification. Progress in Computer Science and Applied Logic, vol 11. Birkhäuser, Boston, MA. https://doi.org/10.1007/978-1-4612-0435-0_7
Download citation
DOI: https://doi.org/10.1007/978-1-4612-0435-0_7
Publisher Name: Birkhäuser, Boston, MA
Print ISBN: 978-1-4612-6758-4
Online ISBN: 978-1-4612-0435-0
eBook Packages: Springer Book Archive