Additional Key Words and Phrases: theorem-proving, resolution, second-order logic, type theory, unification, matching
Selected papers that cite this one
- G. P. Huet. A unification algorithm for typed lambda-calculus. Theoretical Computer Science, 1(1):27-57, June 1975.
- Manfred Schmidt-Schauß A decision algorithm for distributive unification. Theoretical Computer Science, 208(1-2):111-148, 28 November 1998.
Selected references
- J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23-41, January 1965.