Unification: a multidisciplinary survey

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.

REFERENCES

• 1: Alfred V. Aho , John E. Hopcroft, The Design and Analysis of Computer Algorithms, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1974
• 2: ANDREWS, P. B. 1971. Resolution in type theory. J. Symbolic Logic 36, pp. 414-432.
• 3: ANDREWS, P. B., AND COHEN, E. L. 1977. Theorem proving in type theory. In Proceedings of International Joint Conference on Artificial Intelligence.
• 4: ANDREWS, P., MILLER, D., COHEN, E., AND PFEN- NING, F. 1984. Automating higher-order logic. Vol. 29. In Automated Theorem Proving: After 25 Years, W. Bledsoe and D. Loveland, Eds. American Mathematical Society, Providence, R.I., Contemporary Mathematics Series.
• 5: Hassan Ait-Kaci, A lattice theoretic approach to computation based on a calculus of partially ordered type structures (property inheritance, semantic nets, graph unification), 1984
• 6: Hassan Aït-Kaci, An algebraic semantics approach to the effective resolution of type equations, Theoretical Computer Science, v.45 n.3, p.293-351, Sept., 1986
• 7: H Aït-Kaci , R Nasr, Login: A logic programming language with built-in inheritance, Journal of Logic Programming, v.3 n.3, p.185-215, Oct. 1986 [doi>10.1016/0743-1066(86)90013-0]
• 8: Franz Baader, The theory of idempotent semigroups is of unification type zero, Journal of Automated Reasoning, v.2 n.3, p.283-286, Aug. 1987 [doi>10.1007/BF02328451]
• 9: BARWlSE, J., AND PERRY, J. 1983. Situations and Attitudes. MIT Press, Cambridge, Mass.
• 10: BATTANI, G., AND MELONI, H. 1973. Interpreteur du langage de programmation PROLOG. Groupe Intelligence Artificielle, Universit~ Aix-Marseille II.
• 11: BAXTER, r. 1973. An efficient unification algorithm. Tech. Rep. No. CS-73-23, Univ. of Waterloo, Waterloo, Ontario, Canada.
• 12: Lewis Denver Baxter, The complexity of unification., 1976
• 13: BAXTER, L. 1978. The undecidability of the third order dyadic unification problem. Inf. Control 38, pp. 170-178.
• 14: R. V. Book , J. H. Siekmann, On unification: Equational theories are not bounded, Journal of Symbolic Computation, v.2 n.4, p.317-324, Dec. 1986 [doi>10.1016/S0747-7171(86)80001-3]
• 15: BOYER, R. S., AND MOORE, J. S. 1972. The sharing of structure in theorem-proving programs. Mach. inteU. 7.
• 16: BRESNAN, Z., AND KAPLAN, R. 1982. Lexicalfunctional grammar: A formal system for grammatical representation. In The Mental Representation of Grammatical Relations, J. Bresnan, Ed. MIT Press, Cambridge, Mass.
• 17: BRUYNOOGHE, M., AND PEREIRA, r. M. 1984. Deduction revision by intelligent backtracking. In Prolog Implementation, J. A. Campbell, Ed. Elsevier, North-Holland, New York.
• 18: Luca Cardelli, A semantics of multiple inheritance., Proc. of the international symposium on Semantics of data types, p.51-67, July 1984, Sophia-Antipolis, France
• 19: T Y Chen , J-L Lassez , G S Port, Maximal unifiable subsets and minimal non-unifiable subsets, New Generation Computing, v.4 n.2, p.133-152, 1986 [doi>10.1007/BF03037439]
• 20: CHURCH, A. 1940. A formulation of the simple theory of types. J. Symbolic Logic 5, pp. 56-68.
• 21: W F. Clocksin , Christopher S. Mellish, Programming in Prolog (2nd ed.), Springer-Verlag New York, Inc., New York, NY, 1984
• 22: Alain Colmerauer, Metamorphosis Grammars, Natural Language Communication with Computers, p.133-189, January 1978
• 23: COLMERAUER, A. 1982a. An interesting subset of natural language. In Logic Programming, K. L. Clark and S. Tfirnlund, Eds. Academic Press, London.
• 24: COLMERAUER, A. 1982b. Prolog and infinite trees. In Logic Programming, K. L. Clark and S. T/irnlund, Eds. Academic Press, Orlando, Fla.
• 25: COLMERAUER, A. 1983. Prolog in ten figures. In Proceedings of the International Joint Conference on Artificial Intelligence.
• 26: COLMERAUER, A., KANOUI, H., AND VAN CANEGHEM, M. 1973. Un systeme de communication homme-machine en Francais. Research Rep. Groupe Intelligence Artificielle, Universit~ Aix- Marseille II.
• 27: CORBIN, J., AND BIDOIT, M. 1983. A rehabilitation of Robinson's unification algorithm. Inf. Process. 83, pp. 73-79.
• 28: COURCELLE, S. 1983. Fundamental properties of infinite trees. Theor. Comput. Sci. 25, pp. 95-169.
• 29: COX, P. T. 1984. Finding backtrack points for intelligent backtracking. In Prolog Implementation, J. A. Campbell, Ed. Elsevier, North-Holland, New York.
• 30: DAHL, V. 1984. More on gapping grammars. In Proceedings of the International Conference on Fifth Generation Computer Systems. Sponsored by Institute for New Generation Computer Technology (ICOT).
• 31: DAHL, V., AND ABRAMSON. 1984. On gapping grammars. in Proceedings of the 2nd International Conference on Logic Programming. Sponsored by Uppsala University, Uppsala, Sweden.
• 32: Veronica Dahl , Patrick Saint-Dizier, Natural Language Understanding, Elsevier Science Inc., New York, NY, 1985
• 33: DARLINGTON, J. 1968. Automatic theorem proving with equality substitutions and mathematical induction. Mach. InteU. 3. Elsevier, New York.
• 34: DARLINGTON, g. 1971. A partial mechanization of second-order logic. Mach. Intell. 6.
• 35: DARLINGTON, J. 1977. Improving the efficiency of higher order unification. In Proceedings of the International Joint Conference on Artifical Intelligence.
• 36: Dennis De Champeaux, About the Paterson-Wegman linear unification algorithm, Journal of Computer and System Sciences, v.32 n.1, p.79-90, Feb. 1986 [doi>10.1016/0022-0000(86)90003-6]
• 37: Cynthia Dwork , Paris C. Kanellakis , John C. Mitchell, On the sequential nature of unification, Journal of Logic Programming, v.1 n.1, p.35-50, June 1984 [doi>10.1016/0743-1066(84)90022-0]
• 38: C Dwork , P Kanellakis , L Stockmeyer, Parallel algorithms for term matching, Proc. of the 8th international conference on Automated deduction, p.416-430, August 1986, Oxford, United Kingdom
• 39: Jay Clark Earley, An efficient context-free parsing algorithm, 1968
• 40: Jay Earley, An efficient context-free parsing algorithm, Communications of the ACM, v.13 n.2, p.94-102, Feb 1970 [doi>10.1145/362007.362035]
• 41: Andreas Eisele , Jochen Dörre, A lexical functional grammar system in PROLOG, Proceedings of the 11th coference on Computational linguistics, August 25-29, 1986, Bonn, Germany [doi>10.3115/991365.991525]
• 42: Andreas Eisele , Jochen Dörre, Unification of disjunctive feature descriptions, Proceedings of the 26th annual meeting on Association for Computational Linguistics, p.286-294, June 07-10, 1988, Buffalo, New York [doi>10.3115/982023.982058]
• 43: F Fages , G Huet, Complete sets of unifiers and matchers in equational theories, Theoretical Computer Science, v.43 n.2-3, p.189-200, July 1986
• 44: FARMER, W. M. 1987. A unification algorithm for second-order monadic terms. Tech. Rep. (forthcoming). The MITRE Corporation, document MTP-253.
• 45: FAY, M. 1979. First order unification in an equational theory. In Proceedings of the 4th Workshop on Automated Deduction, Austin, Texas.
• 46: GALLIER, J. H., AND SNYDER, W. 1988. Complete sets of transformations for general E-unification. Tech. Rep. MS-CIS-88-72-LINCLAB-130. Dept. of Computer and Information Science, Univ. of Pennsylvania, Philadelphia, Pa.
• 47: GAZDAR, G. 1987. The new grammar formalisms A tutorial survey (abstract). In Proceedings of the International Joint Conference on Artificial Intelligence.
• 48: GAZDAR, G., AND PULLUM, G. K. 1985. Computationally relevant properties of natural languages and their grammars. New Generation Comput. 3, pp. 273-306.
• 49: Gerald Gazdar , Roger Evans , Alex Franz , Karen Osborne, Natural Language Processing in the 1980s: A Bibliography, CSLI Publications, Stanford, CA, 1987
• 50: GOGUEN, J. A., AND MESEGUER, J. 1987. Ordersorted algebra solves the constructor-seleclor multiple representation and coercion problems. Tech. Rep. CSLI-87-92, Center for the Study of Language and Information.
• 51: GOLDFARB, W. D. 1981. The undecidability of the second order unification problem. J. Theoret. Comput. Sci. 13, pp. 225-230.
• 52: Leslie M. Goldschlager, A unified approach to models of synchronous parallel machines, Proceedings of the tenth annual ACM symposium on Theory of computing, p.89-94, May 01-03, 1978, San Diego, California, United States [doi>10.1145/800133.804336]
• 53: GOULD, W. E. 1966a. A matching procedure for w-order logic. Ph.D. dissertation. Princeton Univ., Princeton, N.J.
• 54: GOULD, W. E. 1966b. A matching procedure for w-order logic. Scientific Rep. 4, AFCRL 66-78i.
• 55: GUARD, J. R. 1964. Automated logic for semi-automated mathematics. Scientific Rep. 1, AFCRL 64-411.
• 56: J. Harland , J. Jaffer, On parallel unification for Prolog, New Generation Computing, v.5 n.3, p.259-279, 1987 [doi>10.1007/BF03037466]
• 57: Kôiti Hasida, Conditioned unification for natural language processing, Proceedings of the 11th coference on Computational linguistics, August 25-29, 1986, Bonn, Germany [doi>10.3115/991365.991388]
• 58: HENKIN, L. 1950. Completeness in the theory of types. J. Symbolic Logic 15, pp. 81-91.
• 59: HERBRAND, J. 1971. Recherches sur la theorie de la demonstration. Ph.D. dissertation. In Logical Writings, W. Goldfarb, Ed. Harvard University Press, Cambridge, Massachusetts.
• 60: HINDLEY, R. 1969. The principal type-scheme of an object in combinatory logic. Trans. Am. Math. Soc. 146.
• 61: HIRSH, S. B. 1986. P-PATR: A compiler for unification-based grammars. Center for the Study of Language and information.
• 62: Gerard Pierre Huet, Constrained resolution: a complete method for higher-order logic., 1972
• 63: HUET, G. 1973a. A mechanization of type theory. In Proceedings of the International Joint Conference on Artificial Intelligence.
• 64: HURT, G. 1973b. The undecidability of unification in third order logic. Inf. Control 22, pp. 257-267.
• 65: HUET, G. 1975. A unification algorithm for typed k-calculus. Theoret. Comput. Sci. I, pp. 27-57.
• 66: HUET, G. 1976. Resolution d'equations dans les langages d'ordre 1, 2 ..... w. Ph.D. dissertation. Univ. de Paris VII, France.
• 67: HUET, G., AND OPPEN, D. 1980. Equations and rewrite rules: A survey. In Formal Language Theory, R. V. Book, Ed. Academic Press, Orlando, Fla.
• 68: JAFFAR, J. 1984. Efficient unification over infinite terms. New Generation Comput. 2, pp. 207-219.
• 69: JENSEN, D. C., AND PIETRZYKOWSKI, T. 1976. Mechanizing w-order type theory through unification. Theoret. Comput. Sci. 3, pp. 123-171.
• 70: D Kapur , P Narendran, NP-completeness of the set unification and matching problems, Proc. of the 8th international conference on Automated deduction, p.489-495, August 1986, Oxford, United Kingdom
• 71: KAPUR, D., KRISHNAMOORTHY, M. $., AND NAREN- DRAN, P. 1982. A new linear algorithm for unification. Tech. Rep. 82CRD-100, General Electric.
• 72: Lauri Karttunen, Features and values, Proceedings of the 22nd annual meeting on Association for Computational Linguistics, p.28-33, July 02-06, 1984, Stanford, California
• 73: Lauri Karttunen, D-PATR: a development environment for unification-based grammars, Proceedings of the 11th coference on Computational linguistics, August 25-29, 1986, Bonn, Germany [doi>10.3115/991365.991386]
• 74: KARTTUNEN, L. 1986b. Radical lexicalism. Tech. Rep. CSLI-86-68, Center for the Study of Language and Information.
• 75: Lauri Karttunen , Martin Kay, Structure sharing with binary trees, Proceedings of the 23rd annual meeting on Association for Computational Linguistics, p.133-136, July 08-12, 1985, Chicago, Illinois [doi>10.3115/981210.981226]
• 76: Robert T. Kasper, A unification method for disjunctive feature descriptions, Proceedings of the 25th annual meeting on Association for Computational Linguistics, p.235-242, July 06-09, 1987, Stanford, California [doi>10.3115/981175.981208]
• 77: Robert T. Kasper , William C. Rounds, A logical semantics for feature structures, Proceedings of the 24th annual meeting on Association for Computational Linguistics, p.257-266, July 10-13, 1986, New York, New York [doi>10.3115/981131.981166]
• 78: KAY, M. 1979. Functional grammar. In 5th Annual Meeting of the Berkeley Linguistic Society. Sponsored by Berkeley Linguistics Society, Berkeley, California.
• 79: Martin Kay, Functional Unification Grammar: a formalism for machine translation, Proceedings of the 22nd annual meeting on Association for Computational Linguistics, p.75-78, July 02-06, 1984, Stanford, California
• 80: KAY, M. 1985a. Parsing in functional grammar. In Natural Language Parsing, D. Dowty, L. Karttuhen, and A. Zwicky, Eds. Cambridge Univ. Press, Cambridge.
• 81: KAY, M. 1985b. Unification in grammar. In Natural Language Understanding and Logic Programming, V. Dahl and P. Saint-Dizier, Eds. Elsevier, North-Holland, New York.
• 82: KIRCHNER, C. 1986. Computing unification algorithms. In I st Symposium on Logic in Computer Science. Co-sponsored by IEEE Computer Society, Technical Committee on Mathematical Foundations of Computing; ACM Special Interest Group for Automata and Computability Theory (SIGACT); Association for Symbolic Logic; European Association for Theoretical Computer Science.
• 83: KNUTH, D., AND BENmX, P. B. 1970. Simple word problems in universal algebra. In Computational Problems in Abstract Algebra, J. Leech, Ed. Pergamon Press, Oxford.
• 84: LEVY, J. 1983. A unification algorithm for concurrent Prolog. In Proceedings of the 2nd Logic Programming Conference. Sponsored by Uppsala University, Uppsala, Sweden.
• 85: LEWIS, H. R., AND STATMAN, R. 1982. Unifiability is complete for co-NLogSpace, info. Process. Lett. 15, pp. 220-222.
• 86: LIVESEY, M., SIEKMANN, J., SZABO, P., AND UNVERICHT, E. 1979. Unification problems for combinations of associativity, commutatitivity, distributivity and idempotence axioms. In Proceedings of the 4th Workshop on Automated Deduction, Austin, Texas.
• 87: LUCCHESI, C. L. 1972. The undecidability of the unification problem for third order languages. Tech. Rep. CSRR 2059, Dept. of Applied Analysis and Computer Science, University of Waterloo, Waterloo, Ontario, Canada.
• 88: David MacQueen , Gordon Plotkin , Ravi Sethi, An ideal model for recursive polymorphic types, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.165-174, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800528]
• 89: MALUSZYNSKI, J., AND KOMOROWSKI, H. J. 1985. Unification-free execution of Horn-clause programs. In Proceedings of the 2nd Logic Programming Symposium. IEEE, New York. (Also, Harvard Univ., Computer Science Dept., Tech. Rep. TR- 10-85, 1985. )
• 90: Heikki Mannila , Esko Ukkonen, On the complexity of unification sequences, Proceedings on Third international conference on logic programming, p.122-133, September 1986, London, United Kingdom
• 91: MARTELLI, A., AND MONTANARI, U. 1976. Unification in linear time and space: A structured presentation. Internal Rep. No. B76-16, Ist. di Elaborazione delle Informazione, Consiglio Nazionale delle Ricerche, Pisa, Italy.
• 92: MARTELLI, A., AND MONTANARI, U. 1977. Theorem proving with structure sharing and efficient unification. In Proceedings of International Joint Conference on Artificial Intelligence. (Also Internal Rep. No. S-77-7, Istituto di Scienze dell'Informazione, Univ. of Pisa, Italy).
• 93: Alberto Martelli , Ugo Montanari, An Efficient Unification Algorithm, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.2, p.258-282, April 1982 [doi>10.1145/357162.357169]
• 94: MATSUMOTO, Y., AND SUGIMURA, R. 1987. A parsing system based on logic programming. In Proceedings of the International Joint Conference on Artificial Intelligence.
• 95: MATSUMOTO, Y., TANAKA, H., HIRAKAWA, H., MIYOSHI, H., ANO YASUKAWA, H. 1983. BUP: A bottom-up parser embedded in Prolog. New Generation Comput. 1, pp. 145-158.
• 96: Stan Matwin , Tomasz Pietrzykowski, Exponential Improvement of Efficient Backtracking: data Structure and Implementation, Proceedings of the 6th Conference on Automated Deduction, p.240-259, June 07-09, 1982
• 97: Michael C. McCord, Slot grammars, Computational Linguistics, v.6 n.1, p.31-43, January-March 1980
• 98: Michael C. McCord, Modular Logic Grammars, Proceedings of the 23rd annual meeting on Association for Computational Linguistics, p.104-117, July 08-12, 1985, Chicago, Illinois [doi>10.3115/981210.981223]
• 99: MESEGUER, J., GOGUEN, J. A., AND SMOLKA, G. 1987. Order-sorted unification. Tech. Rep. CSLI-87-86, Center for the Study of Language and Information.
• 100: Dale A. Miller , Gopalan Nadathur, Some uses of higher-order logic in computational linguistics, Proceedings of the 24th annual meeting on Association for Computational Linguistics, p.247-256, July 10-13, 1986, New York, New York [doi>10.3115/981131.981165]
• 101: MILNER, R. 1978. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, pp. 348-375.
• 102: MINSKY, M. 1975. A framework for representing knowledge. In The Psychology of Computer Vision, P. Winston, Ed. McGraw-Hill, New York.
• 103: Tom Michael Mitchell, Version spaces: an approach to concept learning., 1979
• 104: M. D. Moshier , W. C. Rounds, A logic for partially specified data structures, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.156-167, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41639]
• 105: MUKAI, K. 1983. A unification algorithm for infinite trees. In Proceedings of the International Joint Conference on Artificial Intelligence.
• 106: MUKAI, K. 1985a. Horn clause logic with parameterized types for situation semantics programming. Tech. Rep. TR-101, ICOT.
• 107: MUKAI, K. 1985b. Unification over complex indeterminates in Prolog. Tech. Rep. TR-113, ICOT.
• 108: K Mukai , H Yasukawa, Complex indeterminates in Prolog and its application to discourse models, New Generation Computing, v.3 n.4, p.441-466, 1985 [doi>10.1007/BF03037080]
• 109: N. J. Nilsson, Principles of artificial intelligence, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1980
• 110: M. S. Paterson , M. N. Wegman, Linear unification, Proceedings of the eighth annual ACM symposium on Theory of computing, p.181-186, May 03-05, 1976, Hershey, Pennsylvania, United States [doi>10.1145/800113.803646]
• 111: PATERSON, M. S., AND WF. GMA~, M. N. 1978. Linear unification. J. Comput. Syst. Sci. 16, pp. 158-167.
• 112: Fernando Pereira, Extraposition grammars, Computational Linguistics, v.7 n.4, p.243-256, October-December 1981
• 113: Fernando C. N. Pereira, A structure-sharing representation for unification-based grammar formalisms, Proceedings of the 23rd annual meeting on Association for Computational Linguistics, p.137-144, July 08-12, 1985, Chicago, Illinois [doi>10.3115/981210.981227]
• 114: PEREIRA, F. C. N. 1987. Grammars and logics of partial information. In Proceedings of the 4th International Conference on Logic Programming. Springer-Verlag, New York.
• 115: Fernando C. N. Pereira , Stuart M. Shieber, The semantics of grammar formalisms seen as computer languages, Proceedings of the 22nd annual meeting on Association for Computational Linguistics, p.123-129, July 02-06, 1984, Stanford, California
• 116: PEREIRA, F. C. N., AND WARREN, D. H. D. 1980. Definite clause grammars for language analysisa survey of the formalism and a comparison with augmented transition networks. Arti{. Intell. 13, pp. 231-278.
• 117: Tomasz Pietrzykowski, A Complete Mechanization of Second-Order Type Theory, Journal of the ACM (JACM), v.20 n.2, p.333-364, April 1973 [doi>10.1145/321752.321764]
• 118: PIETRZYKOWSKI, T., AND JENSEN, D. 1972. A complete mechanization of w-order logic. Research Rep. CSRR 2060, Univ. of Waterloo, Waterloo, Ontario, Canada.
• 119: PIETRZYKOWSKI, T., AND JENSEN, D. 1973. Mechanizing w-order type theory through unification. Tech. Rep. CS-73-16, Univ. of Waterloo, Waterloo, Ontario, Canada.
• 120: Tomasz Pietrzykowski , Stan Matwin, Exponential Improvement of Efficient Backtracking: A Strategy for Plan-Based Deduction, Proceedings of the 6th Conference on Automated Deduction, p.223-239, June 07-09, 1982
• 121: PLAISTED, D. 1984. The occur-check problem in Prolog. New Generation Comput. 2, pp. 309-322.
• 122: PLOTKIN, G. 1970. A note on inductive generalization. Mach. InteU. 5.
• 123: PLOTKIN. G. 1972. Building-in equational theories. Mach. Intell. 7.
• 124: POLLARD, C. 1985. Phrase structure grammar without metarules. In Proceedings of the 4th West Coast Conference on Formal Linguistics.
• 125: REYLE, U., AND FREY, W. 1983. A PROLOG implementation of lexical functional grammar. In Proceedings of the International Joint Conference on Artificial Intelligence.
• 126: REYNOLDS, J. C. 1970. Transformational systems and the algebraic structure of atomic formulas. Mach. InteU. 5.
• 127: Eric Sven Ristad, Revised generalized phrase structure grammar, Proceedings of the 25th annual meeting on Association for Computational Linguistics, p.243-250, July 06-09, 1987, Stanford, California [doi>10.3115/981175.981209]
• 128: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 129: ROBINSON, J. A. 1968. New directions in mechanical theorem proving. In Proceedings of the International Federation of Information Processing Congress.
• 130: ROBINSON, J. A. 1969. Mechanizing higher-order logic. Mach. InteU. 4.
• 131: ROBINSON, J. A. 1970. A note on mechanizing higher order logic. Mach. InteU. 5.
• 132: ROBINSON, J. A. 1971. Computational logic: The unification computation. Mach. InteU. 6.
• 133: ROBINSON, P. 1985. The SUM: An AI coprocessor. Byte 10.
• 134: ROUNDS, W. C., AND KASPER, R. 1986. A complete logical calculus for record structures representing linguistic information. In Proceedings of the 1st Symposium on Logic in Computer Science. Cosponsored by the IEEE Computer Society, Technical Committee on Mathematical Foundations of Computing; ACM Special Interest Group for Automata and Computability Theory (SIGACT); Association for Symbolic Logic; European Association for Theoretical Computer Science.
• 135: William C. Rounds , Alexis Manaster-Ramer, A logical version of functional grammar, Proceedings of the 25th annual meeting on Association for Computational Linguistics, p.89-96, July 06-09, 1987, Stanford, California [doi>10.3115/981175.981188]
• 136: ROUSSEL, P. 1975. PROLOG, Manuel de reference et d'utilisation. Groupe Intelligence Artificielle, Universit6 Aix-Marseille II.
• 137: SAG, I. A., AND POLLARD, C. 1987. Head-driven phrase structure grammar: An informal synopsis. Tech. Rep. CSLI-87-79, Center for the Study of Language and Information.
• 138: Manfred Schmidt-Schauss, Unification under associativity and idempotence is of type nullary, Journal of Automated Reasoning, v.2 n.3, p.277-281, Aug. 1987 [doi>10.1007/BF02328450]
• 139: SELLS, P. 1985. Lectures on Contemporary Syntactic Theories. Univ. of Chicago, Chicago, Ill. Also, CSLI Lecture Notes Series.
• 140: SHAPIRO, E. 1983. A subset of concurrent Prolog and its interpreter. Tech. Rep. TR-003, ICOT.
• 141: Stuart M. Shieber, The design of a computer language for linguistic information, Proceedings of the 22nd annual meeting on Association for Computational Linguistics, p.362-366, July 02-06, 1984, Stanford, California
• 142: Stuart M. Shieber, Using restriction to extend parsing algorithms for complex-feature-based formalisms, Proceedings of the 23rd annual meeting on Association for Computational Linguistics, p.145-152, July 08-12, 1985, Chicago, Illinois [doi>10.3115/981210.981228]
• 143: SHIEBER, S. 1986. An Introduction to Unification- Based Approaches to Grammar. CSLI Lecture Notes Series, Center for the study of Language and information, Stanford, California.
• 144: Jörg H. Siekmann, Universal Unification, Proceedings of the 7th International Conference on Automated Deduction, p.1-42, May 14-16, 1984
• 145: SIEKMANN, J. 1986. Unification theory. In Proceedings of the 7th European Conference on Artificial Intelligence. Sponsored by the European Coordinating Committee for Artificial Intelligence.
• 146: Gert Smolka , Hassan Ait-Kac, Inheritance hierarchies: semantics and unification, Journal of Symbolic Computation, v.7 n.3-4, p.343-370, March/April 1989 [doi>10.1016/S0747-7171(89)80016-1]
• 147: STABLER, E. P. 1983. Deterministic and bottom-up parsing in Prolog. In Proceedings of the Conference of the American Association for Artificial Intelligence.
• 148: Guy L. Steele, Jr., Common LISP: the language, Digital Press, Newton, MA, 1984
• 149: Mark Edward Stickel, Mechanical theorem proving and artificial intelligence languages., 1977
• 150: Masaru Tomita, An efficient augmented-context-free parsing algorithm, Computational Linguistics, v.13 n.1-2, p.31-46, January-June 1987
• 151: TOMITA, M. 1985a. An efficient context-free parsing algorithm for natural languages. In Proceedings of the International Joint Conference on Artificial Intelligence.
• 152: Masaru Tomita, An efficient context-free parsing algorithm for natural languages and its applications, 1985
• 153: TOMITA, M., AND KNIGHT, g. 1988. Full unification and pseudo unification. Tech. Rep. CMU-CMT- 87-MEMO. Center for Machine Translation, Carnegie-Mellon Univ., Pittsburgh, Pa.
• 154: TRUM, P., AND WINTERSTEIN, G. 1978. Description, implementation, and practical comparison of unification algorithms. Internal Rep. No. 6/78, Fachbereich Informatik, Universitat Kaiserlautern, W. Germany.
• 155: Hans Uszkoreit, Categorial unification grammars, Proceedings of the 11th coference on Computational linguistics, August 25-29, 1986, Bonn, Germany [doi>10.3115/991365.991422]
• 156: M. H. Van Emden , R. A. Kowalski, The Semantics of Predicate Logic as a Programming Language, Journal of the ACM (JACM), v.23 n.4, p.733-742, Oct. 1976 [doi>10.1145/321978.321991]
• 157: VENTURINI-ZILLI, M. 1975. Complexity of the unification algorithm for first-order expressions. Res. Rep. Consiglio Nazionale Delle Ricerche Istituto per le applicazioni del calcolo, Rome, Italy.
• 158: Jeffrey Scott Vitter , Roger A. Simons, Parallel algorithms for unification and other complete problems in p, Proceedings of the 1984 annual conference of the ACM on The fifth generation challenge, p.75-84, January 1984 [doi>10.1145/800171.809607]
• 159: J S Vitter , R A Simons, New classes for parallel complexity: A study of unification and other complete problems P, IEEE Transactions on Computers, v.35 n.5, p.403-418, May 1986 [doi>10.1109/TC.1986.1676783]
• 160: C Walther, A classification of many-sorted unification problems, Proc. of the 8th international conference on Automated deduction, p.525-537, August 1986, Oxford, United Kingdom
• 161: David H D Warren , Luis M. Pereira , Fernando Pereira, Prolog - the language and its implementation compared with Lisp, Proceedings of the 1977 symposium on Artificial intelligence and programming languages, p.109-115, August 15-17, 1977
• 162: WINTERSTEIN, G. 1976. Unification in second order logic. Res. Rep. Fachbereich Informatik, Universitat Kaiserslautern, W. Germany.
• 163: WITTENBURG, K. 1986. Natural language parsing with combinatory categorial grammar in a graphunification-based formalism. Ph.D. dissertation. Univ. of Texas, Austin, Texas.
• 164: W. A. Woods, Transition network grammars for natural language analysis, Communications of the ACM, v.13 n.10, p.591-606, Oct. 1970 [doi>10.1145/355598.362773]
• 165: WROBLEWSKI, D. 1987. Nondestructive graph unification. In Proceedings of the Conference on the American Association for Artificial Intelligence.
• 166: YASUURA, H. 1984. On the parallel computational complexity of unification. In Fifth Generation Computer Systems. Sponsored by. the Institute for New Generation Computer Technology (ICOT). (Also Yajima Labs, Tech. Rep. ER-83- 01, 1983.)
• 167: YOKOI, T., MUKAI, K., MIYOSHI, H., TANAKA, Y., AND SUGIMURA, R. 1986. Research activities on natural language processing of the FGCS project. ICOT J. 14, pp. 1-8.
• 168: ZEEVAT, H., KLEIN, E., AND CALDER, J. 1987. Unification categorial grammar. In Categorial Grammar, Unification Grammar, and Parsing, N. Haddock, E. Klein, and G. Morrill, Eds. Centre for Cognitive Science, University of Edinburgh, Edinburgh, Scotland.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE

Additional Classification:
  E. Data
  E.1 DATA STRUCTURES
      Subjects: Graphs and networks

  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Pattern matching

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.3 Languages and Systems
          Subjects: Substitution mechanisms**
  I.2 ARTIFICIAL INTELLIGENCE

General Terms:
Algorithms, Languages