×

zbMATH — the first resource for mathematics

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.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q65 Abstract data types; algebraic specification
68W30 Symbolic computation and algebraic computation
PDF BibTeX XML Cite
Full Text: DOI
References:
[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, () · Zbl 0551.68075
[3] Ballard, D.; Brown, Ch., ()
[4] Barrow, Ambler; Burstall, Some techniques for recognizing structures in pictures, ()
[5] Barwise, J.; Perry, J., ()
[6] Beilken, Ch.; Mattern, F.; Spenke, M., Entwurf und implementierung von CSSA, vol. A-E, ()
[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, () · Zbl 0656.68102
[9] Blair, F., SCRATCHPAD/1: an interactive facility for symbolic mathematics, ()
[10] Bobrow, D.; Winograd, T.; Buchberger, B., History and basic features of the critical-pair completion procedure, Cognitive science, Journal of symbolic computation, vol 3, no 1, (1987)
[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, (), 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., ()
[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., ()
[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., ()
[20] 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, () · 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., ()
[25] Corneil, D.G., ()
[26] Date, C.J., ()
[27] Davis, M., Eliminating the irrelevant from mechanical proofs, () · Zbl 0131.01201
[28] Davis, M., ()
[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, ()
[32] Forgy, C., OPS5 user manual, ()
[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., ()
[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, () · Zbl 0498.03018
[38] Goguen, J.A.; Meseguer, J., Eqlog: equality, types and generic modules for logic programming, () · 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., ()
[41] Guard, J.R., Automated logic for semi-automated mathematics, (), 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, ()
[44] Hewitt, C., Description and theoretical analysis of PLANNER, a language for proving theorems and manipulation models in a robot, ()
[45] ()
[46] Howie, J., ()
[47] Huet, G.; Oppen, D., Equations and rewirte rules, ()
[48] ICOT, ()
[49] Kamp, H., A theory of truth and semantic representation, ()
[50] Kowalski, R., Logic for problem solving, (1979), North Holland · Zbl 0426.68002
[51] Kozen, D., Complexity of finitely presented algebras, () · Zbl 0824.68076
[52] Loveland, D., ()
[53] Manna, Z.; Waldinger, R., How to clear a block: plan formation in situational logic, () · Zbl 0609.68063
[54] Manove, Bloom; Engelmann, Rational functions in MATHLAB, ()
[55] Markov, A.A., (), 1038, NR 17
[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, ()
[58] Moore, J.S., Computational logic: structure sharing, ()
[59] Moses, J., Symbolic integration: the stormy decade, Cacm, 14, 8, (1971) · Zbl 0228.68009
[60] Moses, J., MACSYMA-the fifth year, ()
[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, () · 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, ()
[67] Rastall, J., Graph family matching, ()
[68] Robinson, J.A., Mechanizing higher order logic, () · Zbl 0228.68025
[69] Rounds, W.C.; Kasper, R., A complete logical calculus for record structures representing linguistic information, ()
[70] Rulifson; Derksen; Waldinger, ()
[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, () · Zbl 0209.01402
[76] Taylor, W., Equational logic, Houston J. of math., 5, (1979)
[77] Tennant, H., Natural language processing, Petrocelli books, (1981)
[78] Touretzky, D.S., The mathematics of inheritance systems, () · 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 Berlin, Heidelberg, N.Y.
[82] Wadge, W., Classified algebras, ()
[83] Wallen, L., Matrix proof methods for modal logics, () · Zbl 0782.03003
[84] Warren, D.H., An abstract prolog instruction set, ()
[85] Winograd, T., Understanding natural language, (1972), Edinburgh Univ. Press
[86] Winograd, T., ()
[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, () · 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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.