Unification theory. (English) Zbl 0678.68098

Summary: Most knowledge based systems in artificial intelligence (AI), with a commitment to a symbolic representation, support one basic operation: “matching of descriptions”. This operation, called unification in work on deduction, is the “addition-and-multiplication” of AI-systems and is consequently often supported by special purpose hardware or by a fast instruction set on most AI-machines. Unification theory provides the formal framework for investigations into the properties of this operation. This article surveys what is presently known in unification theory and records its early history.


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q65 Abstract data types; algebraic specification
68W30 Symbolic computation and algebraic computation
Full Text: DOI


[1] Andrews, P., Resolution in Type Theory, J. of Symbolic Logic, vol. 36 (1971) · Zbl 0231.02038
[2] Andrews, P.; Miller, D.; Cohen, E.; Pfenning, F., Automating Higher Order Logic, (Contemporary Mathematics (1984), American Math Soc) · Zbl 0551.68075
[3] Ballard, D.; Brown, Ch., (Computer Vision (1982), Prentice Hall: Prentice Hall New Jersy)
[4] Barrow, Ambler; Burstall, Some techniques for recognizing Structures in Pictures, (Frontiers of Pattern Recognition (1972), Academic Press Inc)
[5] Barwise, J.; Perry, J., (Situations and Attitudes (1983), MIT Press: MIT Press Cambrdige) · Zbl 0946.03007
[6] Beilken, Ch.; Mattern, F.; Spenke, M., Entwurf und Implementierung von CSSA, vol. A-E, (SEKI-Memo-82-03 (1982), University of Kaiserslautern)
[7] Birkhoff, G., On the Structure of Abstract Algebras, Proc. Cambridge Phil. Soc., vol. 31 (1935) · Zbl 0013.00105
[8] Bläsius, K. H.; Siekmann, J., Partial Unification for Graph based Equational Reasoning, (Proc. of 9th Intern. Conf. on Automated Deduction, Springer LNCS, vol. 310 (1988)) · Zbl 0656.68102
[9] Blair, F., SCRATCHPAD/1: An interactive Facility for Symbolic Mathematics, (Proc. of the 2nd Symposium on Symbolic Manipulation. Proc. of the 2nd Symposium on Symbolic Manipulation, Los Angeles (1971))
[10] Buchberger, B., History and Basic Features of the Critical-Pair Completion Procedure, Journal of Symbolic Computation, vol 3, no 1 (1987) · Zbl 0645.68094
[11] Böhm, H. P.; Fischer, H. L.; Raulefs, P., CSSA: Language Concepts and Programming M. 1977 (1977)
[12] Book, R., Thue Systems as Rewriting Systems, (Proc. of Rewriting Techniques (1985), Springer Lecture Notes in Comp. Sci.), vol. 202 · Zbl 0587.03026
[13] Boyer, R.; Moore, J. S., A Fast String Searching Algorithm, CACM, vol. 20, no. 10 (1977) · Zbl 1219.68165
[14] Brachman, R.; Levesque, H., (Readings in Knowledge Representation (1985), Will. Kaufmann Inc) · Zbl 0609.68007
[15] Brachman, R.; Schmolze, J., An Overview of KL-ONE, Cognitive Science, vol. 9, no. 2 (1985)
[16] Bryan, H.; Carnog, J., Search Methods used with Transistor Patent Applications, IEEE Spectrum, 3, 2 (1966)
[17] Buchanan, B.; Shortliffe, R., (Rule Based Expert Systems (1985), Addison Wesley)
[18] Buchberger, B., History and Basic Features of the Critical-Pair Completion Procedure, Journal of Symbolic Computation, vol. 3, no. 1 (1987) · Zbl 0645.68094
[19] Burris, S.; Sankappanavar, H. P., (A Course in Universal Algebra (1981), Springer Verlag) · Zbl 0478.08001
[20] CADE see: Proceedings of the International Conference on Automated Deduction, SpringerLecture Notes in Computer Science, biannually, Springer Verlag.; CADE see: Proceedings of the International Conference on Automated Deduction, SpringerLecture Notes in Computer Science, biannually, Springer Verlag.
[21] Cardelli, L., A Semantics of Multiple Inheritance, (Proc. of Symposium on Semantics of Data Types. Proc. of Symposium on Semantics of Data Types, Springer LNCS, vol. 173 (1984)) · Zbl 0543.68011
[22] Church, A., A Formulation of the Simple Theory of Types, Journal of Symbolic Logic, vol. 5 (1940) · JFM 66.1192.06
[23] Clifford, A.; Preston, G., The Algebraic Theory of Semigroups, vol. I and vol. II (1961) · Zbl 0111.03403
[24] Clocksin, W.; Mellish, C., (Programming in PROLOG (1981), Springer) · Zbl 0466.68009
[25] Corneil, D. G., (“Graph Isomorphism”, Ph.D. (1968), Dept. of Computer Science, University of Toronto)
[26] Date, C. J., (An Introduction to Database Systems (1976), Addison-Wesley Publ. Comp. Inc.) · Zbl 1058.68045
[27] Davis, M., Eliminating the Irrelevant from Mechanical Proofs, (Symposia of Applied Math, vol. 15 (1963), American Mathematical Society) · Zbl 0131.01201
[28] Davis, M., (The Undecidable (1965), Raven Press: Raven Press Hewlett, New York)
[29] Dickson, L., Finiteness of the Odd Perfect and Primitive Abundant Numbers, Amer. Journal of Maths, vol 35 (1913) · JFM 44.0220.02
[30] Farber, D. J.; Griswald, R. E.; Polonsky, I. P., SNOBOL as String Manipulation Language, JACM, vol. 11, no. 2 (1964) · Zbl 0117.12201
[31] Fateman, R., The User-Level Semantic Matching Capability in MACSYMA, (Proc. of the 2nd Symposium on Symbolic Manipulation. Proc. of the 2nd Symposium on Symbolic Manipulation, Los Angeles (1971))
[32] Forgy, C., OPS5 User Manual, (Techn. Report, CMU-CS-81-135 (1981), Carnegie Mellon University)
[33] Forgy, C., Rete: A Fast Algorithm for the Many Pattern/Object Match Problem, J. of Art. Intelligence, vol. 19, no. 1 (1982)
[34] Gabriel, J., A Tutorial on the Warren Abstract Machine, Argonne National Lab., ANL-84-84 (1984)
[35] Gallaire, H.; Minker, J., (Logic and Databases (1978), Plenum Press)
[36] Goguen, J. A.; Thatcher, J.; Wagner, E.; Wright, J., Initial Algebra Semantics and Continuous Algebras, JACM, vol. 24, no. 1 (1977) · Zbl 0359.68018
[37] Goguen, J. A., Order sorted algebra, (Techn. Report No 14 (1978), UCLA, Comp. Sci. Dept.) · Zbl 0498.03018
[38] Goguen, J. A.; Meseguer, J., Eqlog: Equality, Types and Generic Modules for Logic Programming, (DeGroot, Lindstrom, Logic Programming, Functions and Equations (1986), Prentice Hall) · Zbl 0498.03018
[39] Gordan, P., Über die Auflösung linearer Gleichungen mit reellen Coefficienten, Mathematische Annalen, 23-28 (1873) · JFM 05.0095.01
[40] Grätzer, G., (Universal Algebra (1979), Springer Verlag) · Zbl 0412.08001
[41] Guard, J. R., Automated Logic for Semi-Automated Mathematics, (Scientific report no. 1 (1964), Air Force Cambridge Research Labs.), AD 602 710 · Zbl 0175.28205
[42] Guard, J. R.; Oglesby, F. C.; Benneth, J. H.; Settle, L. G., Semi-Automated Mathematics, JACM, vol. 18, no. 1 (1969) · Zbl 0175.28205
[43] Hearn, A., REDUCE2, A System and Language for Algebraic Manipulation, (Proc. of the 2nd Symposium on Symbolic Manipulation. Proc. of the 2nd Symposium on Symbolic Manipulation, Los Angeles (1971))
[44] Hewitt, C., Description and Theoretical Analysis of PLANNER, a Language for Proving Theorems and Manipulation Models in a Robot, (Dept. of Mathematics, Ph.C. Thesis (1972), MIT)
[45] (Hoare, C. R.A.; Shepherdson, J. C., Mathematical Logic and Programming Languages (1985), Prentice Hall) · Zbl 0626.68003
[46] Howie, J., (Introduction to Semigroup Theory (1976), Academic Press) · Zbl 0355.20056
[47] Huet, G.; Oppen, D., Equations and Rewirte Rules, (Book, R., Formal Language Theory: Perspectives and Open Problems (1980), Academic Press: Academic Press New York)
[48] ICOT, (Fifth Generation Computer Systems (1984), North Holland Publ. Comp) · Zbl 0577.68001
[49] Kamp, H., A Theory of Truth and Semantic Representation, (Groenendijk, J.; etal., Formal Methods in the Study of Language (1981), Mathematical Centre: Mathematical Centre Amsterdam)
[50] Kowalski, R., Logic for Problem Solving (1979), North Holland · Zbl 0426.68002
[51] Kozen, D., Complexity of finitely presented algebras, (Int. Report 76-294 (1976), Dept. of Comp. Sci, Cornell University) · Zbl 0824.68076
[52] Loveland, D., (Automated Theorem Proving (1978), North Holland) · Zbl 0364.68082
[53] Manna, Z.; Waldinger, R., How to clear a block: Plan formation in situational logic, (Proc. CADE, Springer LNCS, vol 230 (1986)) · Zbl 0609.68063
[54] Manove, Bloom; Engelmann, Rational Functions in MATHLAB, (IFIP Conf on Symb. Manipulation. IFIP Conf on Symb. Manipulation, Pisa (1968))
[55] Markov, A. A., (Trudy Mat. Inst. Steklov, no. 42 (1954), Izdat. Akad. Nauk SSSR), 1038, NR 17 · Zbl 0058.00501
[56] McNulty, G., The Decision Problem of Equational Bases of Algebras, Annals of Mathem. Logic, vol. 10 (1976) · Zbl 0376.08005
[57] Minsky, M., A Framework for Representing Knowledge, (P., Winston, The Psychology of Computer Vision (1975), McGraw Hill)
[58] Moore, J. S., Computational Logic: Structure Sharing, (Th.D. thesis (1973), Univ. of Edinburgh)
[59] Moses, J., Symbolic Integration: The Stormy Decade, CACM, 14, 8 (1971) · Zbl 0228.68009
[60] Moses, J., MACSYMA-the fifth Year, (Project MAC (1974), MIT: MIT Cambridge)
[61] Nelson, G.; Oppen, D., Fast Decision Procedures based on Congruence Closure, JACM, 356-364 (1980) · Zbl 0441.68111
[62] Nevins, A., A Human Oriented Logic for ATP, JACM, 21 (1974)
[63] Oberschelp, A., Untersuchungen zur mehrsortigen Quantorenlogik, Mathematische Annalen, vol. 145, 297-333 (1962) · Zbl 0101.25001
[64] Ohlbach, H. J., A Resolution Calculus for Modal Logics, (Ph.D. thesis (1988), Universität Kaiserslautern) · Zbl 0746.03010
[65] Prawitz, D., An Improved Proof Procedure, Theoria, 26 (1960) · Zbl 0099.00801
[66] Ramnarayan, R.; Zimmermann, G., PESA, A Parallel Architecture for OPS5 Production Systems, (19th Annual Hawaii International Conference on Systems Sciences (1985))
[67] Rastall, J., Graph Family Matching, (MIP-R-62 (1969), University of Edinburgh)
[68] Robinson, J. A., Mechanizing Higher Order Logic, (Machine Intelligence, vol 4 (1969), Edinburgh Univ. Press) · Zbl 0228.68025
[69] Rounds, W. C.; Kasper, R., A Complete Logical Calculus for Record Structures Representing Linguistic Information, (Proc. of IEEE Symp. on Logic in Comp. Sci. (1986))
[70] Rulifson; Derksen; Waldinger, (QA4: A Procedural Calculus for Intuitive Reasoning, Nov. (1972), Stanford Univ.)
[71] Shostak, R., Deciding Combinations of Theories, JACM, vol. 31, no. 1 (1985), Springer Lecture Notes Comp. Sci., vol. 87 · Zbl 0481.68089
[72] Siekmann, J.; Szabo, P., A Noetherian and Complete Rewirte System for Idempotent Semigroups, Semigroup Forum, vol. 25 (1982) · Zbl 0493.68087
[73] Slagle, J. R., ATP with built-in Theories including Equality, Partial Ordering and Sets, JACM, 19, 120-135 (1972) · Zbl 0231.68035
[74] Sussenguth, A., A Graph-theoretical Algorithm for Matching Chemical Structures, J. Chem. Doc., 5, 1 (1965)
[75] Tarski, A., Equational Logic and Equational Theories of Algebra, (Schmidt; etal., Contributions to Mathematical Logic (1968), North Holland) · Zbl 0209.01402
[76] Taylor, W., Equational Logic, Houston J. of Math., 5 (1979) · Zbl 0421.08004
[77] Tennant, H., Natural Language Processing, Petrocelli Books (1981)
[78] Touretzky, D. S., The mathematics of Inheritance Systems, (Research Notes in Art. Intelligence (1987), M. Kaufman, Publishers: M. Kaufman, Publishers Los Altos) · Zbl 0675.68006
[79] Ullman, J. R., An Algorithm for Subgraph Isomorphism, JACM, vol. 23, no. 1 (1976) · Zbl 0323.05138
[80] Unger, S. H., GIT-Heuristic program for Testing Pairs of Directed Line Graphs for Isomorphism, CACM, vol. 7, no. 1 (1964) · Zbl 0123.33710
[81] van Wijngaarden, Revised Rep. on the Algorithmic Language ALGOL68 (1976), Springer Verlag: Springer Verlag Berlin, Heidelberg, N.Y. · Zbl 0327.68007
[82] Wadge, W., Classified Algebras, (Internat. Report No 46 (1982), Univ. of Warwick: Univ. of Warwick England)
[83] Wallen, L., Matrix Proof Methods for Modal Logics, (Proc. of Intern. Joint Conf. on Art. Intelligence. Proc. of Intern. Joint Conf. on Art. Intelligence, Milan, Italy (1987)) · Zbl 0782.03003
[84] Warren, D. H., An Abstract Prolog Instruction Set, (SRI Technical Note 309 (1983), SRI-International)
[85] Winograd, T., Understanding Natural Language (1972), Edinburgh Univ. Press
[86] Winograd, T., (Language as a Cognitive Process, vol. 1 (1983), Addison Wesley) · Zbl 0505.68032
[87] Winston, P., The Psychology of Computer Vision (1975), McGraw Hill
[88] Wos, L.; Robinson, G. A.; Carson, D.; Shalla, L., The Concept of Demodulation in Theorem Proving, JACM, vol. 14, no. 4 (1967) · Zbl 0157.02501
[89] Wos, L.; Robinson, G. A., Maximal Models and Refutation Completeness: Semidecision Procedures in Automatic Theorem Proving, (Boone, W. W.; Cannonito, F. B.; Lyndon, R. C., Word Problems (1973), North Holland) · Zbl 0283.68058
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.