Unification under a mixed prefix
Author:
- Dale MillerDMDale Miller
- 1 October 1992
- journal article
- Published by Elsevier in Journal of Symbolic Computation
- Vol. 14 (4) , 321-358
Abstract
No abstract availableKeywords
This publication has 16 references indexed in Scilit:
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple UnificationJournal of Logic and Computation, 1991
- Higher-order Horn clausesJournal of the ACM, 1990
- Higher-order unification revisited: Complete sets of transformationsJournal of Symbolic Computation, 1989
- Natural deduction as higher-order resolutionThe Journal of Logic Programming, 1986
- The undecidability of the second-order unification problemTheoretical Computer Science, 1981
- Mechanizing ω-order type theory through unificationTheoretical Computer Science, 1976
- General models and extensionalityThe Journal of Symbolic Logic, 1972
- Resolution in type theoryThe Journal of Symbolic Logic, 1971
- Completeness in the theory of typesThe Journal of Symbolic Logic, 1950
- A formulation of the simple theory of typesThe Journal of Symbolic Logic, 1940