Unification: a multidisciplinary survey
- 1 March 1989
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Computing Surveys
- Vol. 21 (1) , 93-124
- https://doi.org/10.1145/62029.62030
Abstract
The unification problem and several variants are presented. Various algorithms and data structures are discussed. Research on unification arising in several areas of computer science is surveyed; these areas include theorem proving, logic programming, and natural language processing. Sections of the paper include examples that highlight particular uses of unification and the special problems encountered. Other topics covered are resolution, higher order logic, the occur check, infinite terms, feature structures, equational theories, inheritance, parallel algorithms, generalization, lattices, and other applications of unification. The paper is intended for readers with a general computer science background—no specific knowledge of any of the above topics is assumed.Keywords
This publication has 41 references indexed in Scilit:
- A theory of type polymorphism in programmingPublished by Elsevier ,2003
- On unification: Equational theories are not boundedJournal of Symbolic Computation, 1986
- Login: a logic programming language with built-in inheritanceThe Journal of Logic Programming, 1986
- Parsing in functional unification grammarPublished by Cambridge University Press (CUP) ,1985
- On the sequential nature of unificationThe Journal of Logic Programming, 1984
- Fundamental properties of infinite treesTheoretical Computer Science, 1983
- The undecidability of the second-order unification problemTheoretical Computer Science, 1981
- Mechanizing ω-order type theory through unificationTheoretical Computer Science, 1976
- A Complete Mechanization of Second-Order Type TheoryJournal of the ACM, 1973
- Resolution in type theoryThe Journal of Symbolic Logic, 1971