Advertisement

Designing Unification Procedures Using Transformations: A Survey

  • Jean H. Gallier
  • Wayne Snyder
Conference paper
Part of the Mathematical Sciences Research Institute Publications book series (MSRI, volume 21)

Abstract

Unification is a very general computational paradigm that plays an important role in many different areas of symbolic computation. For example, unification plays a central role in
  • Automated Deduction (First-order logic with or without equality, higher-order logic);

  • Logic Programming (Prolog, λ-Prolog);

  • Constraint-based Programming;

  • Type Inferencing (ML, ML+, etc.);

  • Knowledge-Base Systems, Feature structures; and

  • Computational Linguistics (Unification grammars).

Keywords

Logic Program Theorem Prove Symbolic Computation Unification Algorithm Ground Term 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Aït-Kaci, H. A lattice theoretic approach to computation based on a calculus of partially ordered type structures, Ph.D. thesis. Department of Computer and Information Science, University of Pennsylvania, PA (1984).Google Scholar
  2. 2.
    Aït-Kaci, H. An algebraic semantics approach to the effective resolution of type equations. Theoretical Computer Science 45, pp. 293–351 (1986).MathSciNetMATHCrossRefGoogle Scholar
  3. 3.
    Andrews, P.B., “Resolution in Type Theory”, JSL 36:3 (1971) 414–432.MATHCrossRefGoogle Scholar
  4. 4.
    Andrews, P . Theorem Proving via General Matings.J.ACM 28(2), 193–214, 1981MATHCrossRefGoogle Scholar
  5. 5.
    Andrews, P. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, New York, 1986.MATHGoogle Scholar
  6. 6.
    Andrews, P.B., D. Miller, E. Cohen, F. Pfenning, “Automating Higher-Order Logic”, Contemporary Mathematics 29, 169–192, 1984.MathSciNetGoogle Scholar
  7. 7.
    Bachmair, L., Proof Methods for Equational Theories, Ph.D thesis, University of Illinois, Urbana Champaign, Illinois (1987).Google Scholar
  8. 8.
    Bachmair, L., Canonical Equational Proofs, Research Notes in Theoretical Computer Science, Wiley and Sons, 1989.Google Scholar
  9. 9.
    Bachmair, L., Dershowitz, N., and Plaisted, D., “Completion without Failure”, Resolution of Equations in Algebraic Structures, Vol. 2, Aït-Kaci and Nivat, editors, Academic Press, 1–30 (1989).Google Scholar
  10. 10.
    Bachmair, L., Dershowitz, N., and Hsiang, J., “Orderings for Equational Proofs”, In Proc. Symp. Logic in Computer Science, Boston, Mass. (1986) 346–357.Google Scholar
  11. 11.
    Barendregt, H.P., The Lambda Calculus, North-Holland (1984).Google Scholar
  12. 12.
    Bibel, W. Tautology Testing With a Generalized Matrix Reduction Method, TCS 8, pp. 31–44, 1979.MathSciNetMATHCrossRefGoogle Scholar
  13. 13.
    Bibel, W . On Matrices With Connections, J.ACM 28, pp. 633–645, 1981. MathSciNetMATHCrossRefGoogle Scholar
  14. 14.
    Bibel, W. Automated Theorem Proving. Friedr. Vieweg & Sohn, Braunschweig, 1982.MATHGoogle Scholar
  15. 15.
    Boudet, A., Jouannaud, J.-P., and Schmidt-Schauss, M. Unification in Boolean Rings and Abelian Groups. Journal of Symbolic Computation 8(5), pp. 449–478 (1989).MathSciNetMATHCrossRefGoogle Scholar
  16. 16.
    Bürckert, H., Herold, A., and Schmidt-Schauss, M. On equational theories, unification, and (un)decidability. Special issue on Unification, Part II, Journal of Symbolic Computation 8(1 & 2), 3–50 (1989).MATHGoogle Scholar
  17. 17.
    Bürckert, H., Matching-A Special Case of Unification? Journal of Symbolic Computation 8(5), pp. 523–536 (1989).MathSciNetMATHCrossRefGoogle Scholar
  18. 18.
    Choi, J., and Gallier, J.H. A simple algebraic proof of the NP-completeness of rigid E-unification, in preparation (1990).Google Scholar
  19. 19.
    Church, A., “A Formulation of the Simple Theory of Types”, JSL 5 (1940) 56–68.MathSciNetMATHCrossRefGoogle Scholar
  20. 20.
    Comon, H. Unification and Disunification. Theorie et Applications, These de l’Tnstitut Polytechnique de Grenoble (1988).Google Scholar
  21. 21.
    Darlington, J.L., “A Partial Mechanization of Second-Order Logic”, Machine Intelligence 6 (1971) 91–100.MATHGoogle Scholar
  22. 22.
    Dershowitz, N, “Termination of Rewriting”, Journal of Symbolic Computation 3(1987) 69–116.MathSciNetMATHCrossRefGoogle Scholar
  23. 23.
    Dougherty, D., and Johann, P., “An Improved General E-Unification Method”, CADE’90, Kaiserslautern, Germany.Google Scholar
  24. 24.
    Elliot, C, and Pfenning, F., “A Family of Program Derivations for Higher-Order Unification”, Ergo Report 87–045, CMU, November 1987.Google Scholar
  25. 25.
    Fages, F. and Huet, G., “Complete Sets of Unifiers and Matchers in Equational Theories”, TCS 43 (1986) 189–200.MathSciNetMATHCrossRefGoogle Scholar
  26. 26.
    Farmer, W., Length of Proofs and Unification Theory, Ph.D. Thesis, University of Wisconsin—Madison (1984).Google Scholar
  27. 27.
    Farmer, W. “A Unification Algorithm for Second-Order Monadic Terms”, Unpublished Technical Report, MITRE Corporation, Bedford, MA.Google Scholar
  28. 28.
    Fay, M., “First-order Unification in an Equational Theory”, Proceedings of the 4th Workshop on Automated Deduction, Austin, Texas (1979).Google Scholar
  29. 29.
    Felty, A., and Miller, D., “Specifying Theorem Provers in a Higher-Order Logic Programming Language”, Ninth International Conference on Automated Deduction, Argonne, Illinois (1988).Google Scholar
  30. 30.
    Gallier, J.H. Logic for Computer Science: Foundations of Automatic Theorem Proving, Harper and Row, New York (1986).MATHGoogle Scholar
  31. 31.
    Gallier, J.H., Raatz, S., “Extending SLD-Resolution to Equational Horn Clauses Using E-unification”, Journal of Logic Programming 6(1–2), 3–56 (1989).MathSciNetMATHCrossRefGoogle Scholar
  32. 32.
    Gallier, J.H., Raatz, S., and Snyder, W., “Theorem Proving using Rigid E-Unification: Equational Matings”, LICS’87, Ithaca, New York (1987) 338–346.Google Scholar
  33. 33.
    Gallier, J.H., Narendran, P., Plaisted, D., Raatz, S., and Snyder, W., “Finding canonical rewriting systems equivalent to a finite set of ground equations in polynomial time”, submitted to J.ACM (1987).Google Scholar
  34. 34.
    Gallier, J.H., Narendran, P., Plaisted, D., and Snyder, W., “Rigid E-unification is NP-complete”, LICS’88, Edinburgh, Scotland, July 5–8, 1988, 218–227.Google Scholar
  35. 35.
    Gallier, J.H., and Snyder, W. Complete Sets of Transformations For General E-Unification. Special issue of Theoretical Computer Science 67(2–3), 203–260 (1989).MathSciNetMATHCrossRefGoogle Scholar
  36. 36.
    Gallier, J.H., Raatz, S, and Snyder, W. Rigid E-Unification and its Applications to Equational Matings. Resolution of Equations in Algebraic Structures, Vol. 1, Ait-Kaci and Nivat, editors, Academic Press, 151–216 (1989). Google Scholar
  37. 37.
    Gallier, J.H., Narendran, P., Plaisted, D., and Snyder, W. Rigid E-Unification: NP-completeness and Applications to Theorem Proving. To appear in a special issue of Information and Computation, pp. 64 (1990).Google Scholar
  38. 38.
    Gallier, J.H., Narendran, P., Raatz, S., and Snyder, W. Theorem Proving Using Equational Matings and Rigid E-Unification. To appear in J.ACM, pp. 62 (1990).Google Scholar
  39. 39.
    Girard, J.Y., “Linear Logic”, Theoretical Computer Science 50:1 (1987) 1–102.MathSciNetMATHCrossRefGoogle Scholar
  40. 40.
    Goguen, J.A. What is Unification? A categorical View of Substitution, Equation and Solution. Resolution of Equations in Algebraic Structures, Vol. 1, Aït-Kaci and Nivat, editors, Academic Press, 217–261 (1989). Google Scholar
  41. 41.
    Goguen, J.A., and Meseguer, J., “Eqlog: Equality, Types, and Generic Modules for Logic Programming”, in Functional and Logic Programming, Degroot, D. and Lind-strom, G., eds., Prentice-Hall (1985). Short version in Journal of Logic Programming 2 (1984) 179–210.Google Scholar
  42. 42.
    Goldfarb, W., “The Undecidability of the Second-Order Unification Problem”, TCS 13:2 (1981) 225–230.MathSciNetMATHCrossRefGoogle Scholar
  43. 43.
    Gould, W.E., A Matching Procedure for Omega-Order Logic, Ph.D. Thesis, Princeton University, 1966.Google Scholar
  44. 44.
    Guard, J.R., “Automated Logic for Semi-Automated Mathematics”, Scientific Report 1, AFCRL 64–411, Contract AF 19 (628)-3250 AD 602 710.Google Scholar
  45. 45.
    Guard, J., Oglesby, J., and Settle, L., “Semi-Automated Mathematics”, JACM 16 (1969) 49–62.MATHCrossRefGoogle Scholar
  46. 46.
    Hannan, J. and Miller, D., “Enriching a Meta-Language with Higher-Order Features”, Workshop on Meta-Programming in Logic Programming, Bristol (1988).Google Scholar
  47. 47.
    Hannan, J. and Miller, D., “Uses of Higher-Order Unification for Implementing Program Transformers”, Fifth International Conference on Logic Programming, MIT Press (1988).Google Scholar
  48. 48.
    Herbrand, J. , “Sur la Théorie de la Demonstration”, in Logical Writings, W. Goldfarb, ed., Cambridge (1971). Google Scholar
  49. 49.
    Hindley, J., and Seidin, J., Introduction to Combinators and Lambda Calculus, Cambridge University Press (1986).MATHGoogle Scholar
  50. 50.
    Huet, G. Constrained Resolution: A Complete Method for Higher-Order Logic, Ph.D. thesis, Case Western Reserve University (1972). Google Scholar
  51. 51.
    Huet, G. , “A Mechanization of Type Theory”, Proceedings of the Third International Joint Conference on Artificial Intelligence (1973) 139–146. Google Scholar
  52. 52.
    Huet, G., “The Undecidability of Unification in Third-Order Logic”, Information and Control 22 (1973) 257–267.MathSciNetMATHCrossRefGoogle Scholar
  53. 53.
    Huet, G., “A Unification Algorithm for Typed λ-Calculus”, TCS 1 (1975) 27–57.MathSciNetCrossRefGoogle Scholar
  54. 54.
    Huet, G., Résolution d’Equations dans les Langages d’Ordre 1,2,…, ω, Thèse d’Etat, Université de Paris VII (1976).Google Scholar
  55. 55.
    Huet, G., and Lang, B., “Proving and Applying Program Transformations Expressed with Second-Order Patterns”, Acta Informatica 11 (1978) 31–55.MathSciNetMATHCrossRefGoogle Scholar
  56. 56.
    Huet, G., “Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems,” JACM 27:4 (1980) 797–821.MathSciNetMATHCrossRefGoogle Scholar
  57. 57.
    Hullot, J.-M. , “Canonical Forms and Unification”, CADE-5 (1980) 318–334. Google Scholar
  58. 58.
    Hussmann, H. , “Unification in Conditional Equational Theories”, Proceedings of the EUROCAL 1985, Springer Lecture Notes in Computer Science 204, p. 543–553. MathSciNetGoogle Scholar
  59. 59.
    Hsiang, J., and Jouannaud, J.-P. General E-unification revisited. In Proceedings of UNIF’88, C. Kirchner and G. Smolka, editors, CRIN Report 89R38, pp. 51 (1988). Google Scholar
  60. 60.
    Isakowitz, T. Theorem Proving Methods For Order-Sorted Logic, Ph.D. thesis. Department of Computer and Information Science, University of Pennsylvania (1989).Google Scholar
  61. 61.
    Jouannaud, J.-P., and Kirchner, C. Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification. Technical Report, University of Paris Sud (1989).Google Scholar
  62. 62.
    Kaplan, S., “Fair Conditional Term Rewriting Systems: Unification, Termination, and Confluence”, Technical Report 194, Universite de Paris-Sud, Centre D’Orsay, Laboratoire de Recherche en Informatique (1984).Google Scholar
  63. 63.
    Kirchner, C , “A New Equational Unification Method: A Generalization of Martelli-Montanari’s Algorithm”, CADE-7, Napa Valley (1984). Google Scholar
  64. 64.
    Kirchner, C, Méthodes et Outils de Conception Systematique d’Algorithmes d’Unification dans les Theories Equationnelles, These d’Etat, Université de Nancy I (1985).Google Scholar
  65. 65.
    Kirchner, C, “Computing Unification Algorithms,” LICS’86, Cambridge, Mass. (1986).Google Scholar
  66. 66.
    Kirchner, C. and Kirchner, H., Contribution a la Resolution d’Equations dans les Algèbres Libres et les Varietes Equationnelles dAlgèbres, These de 3e cycle, Université de Nancy I (1982).Google Scholar
  67. 67.
    Kfoury, A.J., J. Tiuryn, and P. Urzyczyn, “An analysis of ML typability”, submitted (a section of this paper will appear in the proceedings of CAAP 1990 under the title “ML typability is DEXPTIME-complete”).Google Scholar
  68. 68.
    Kfoury, A.J., J. Tiuryn, and P. Urzyczyn, “The undecidability of the semi-unification problem”, Proceedings of STOC (1990).Google Scholar
  69. 69.
    Kfoury, A.J., and J. Tiuryn, “Type Reconstruction in Finite-Rank Fragments of the Polymorphic Lambda Calculus”, LICS’90, Philadelpha, PA.Google Scholar
  70. 70.
    Knight. K. “A Multidisciplinary Survey”, ACM Computing Surveys, Vol. 21, No. 1, pp. 93–124 (1989). MathSciNetCrossRefGoogle Scholar
  71. 71.
    Knuth, D.E. and Bendix, P.B., “Simple Word Problems in Univeral Algebras”, in Computational Problems in Abstract Algebra, Leech, J., ed., Pergamon Press (1970). Google Scholar
  72. 72.
    Kozen, D., “Complexity of Finitely Presented Algebras,” Technical Report TR 76–294, Department of Computer Science, Cornell University, Ithaca, New York (1976).Google Scholar
  73. 73.
    Kozen, D., “Positive First-Order Logic is NP-Complete”, IBM Journal of Research and Development, 25:4 (1981) 327–332.MathSciNetMATHCrossRefGoogle Scholar
  74. 74.
    Lankford, D.S. , “Canonical Inference”, Report ATP-32, University of Texas (1975). Google Scholar
  75. 75.
    Lassez, J.-L., Mäher, M., and Marriot, K. Unification Revisited. Foundations of Deductive Databases and Logic Programming, J. Minker, editor, Morgan-Kaufman, pp. 587–625 (1988).Google Scholar
  76. 76.
    Le Chenadec, P. On the Logic of Unification. Special issue on Unification, Part II, Journal of Symbolic Computation 8(1 & 2), 141–200 (1989).MATHGoogle Scholar
  77. 77.
    Lucchesi, C.L., “The Undecidability of the Unification Problem for Third Order Languages”, Report CSRR 2059, Dept. of Applied Analysis and Computer Science, University of Waterloo (1972).Google Scholar
  78. 78.
    Machtey, M. and Young, P.R., An Introduction to the General Theory of Algorithms, Elsevier North-Holland, NY, 1977.Google Scholar
  79. 79.
    Martelli, A., Montanari, U., “An Efficient Unification Algorithm”, ACM Transactions on Programming Languages and Systems, 4:2 (1982) 258–282.MATHCrossRefGoogle Scholar
  80. 80.
    Martelli, A., Rossi, G.F., and Moiso, C. Lazy Unification Algorithms for Canonical Rewrite Systems. Resolution of Equations in Algebraic Structures, Vol. 2,Aït-Kaci and Nivat, editors, Academic Press, 245–274(1989).Google Scholar
  81. 81.
    Meseguer, J., Goguen, J. A., and Smolka, G. Order-Sorted Unification. Journal of Symbolic Computation 8(4), pp. 383–413 (1989).MathSciNetMATHCrossRefGoogle Scholar
  82. 82.
    Miller, D., Proofs in Higher-Order Logic, Ph.D. thesis, Carnegie-Mellon University, 1983.Google Scholar
  83. 83.
    Miller, D. A. Expansion Trees and Their Conversion to Natural Deduction Proofs. In 7th International Conference on Automated Deduction, Napa, CA, edited by R.E. Shostak, L.N.CS, No. 170, New York: Springer Verlag, 1984.Google Scholar
  84. 84.
    Miller, D. A compact Representation of Proofs. Studia Logica 4/87, pp. 347–370 (1987).CrossRefGoogle Scholar
  85. 85.
    Miller, D., and Nadathur, G., “Higher-Order Logic Programming”, Proceedings of the Third International Conference on Logic Programming, London (1986).Google Scholar
  86. 86.
    Miller, D., and Nadathur, G., “A Logic Programming Approach to Manipulating Formulas and Programs”, IEEE Symposium on Logic Programming, San Franciso (1987).Google Scholar
  87. 87.
    Miller, D., and Nadathur, G., “Some Uses of Higher-Order Logic in Computational Linguistics”, 24th Annual Meeting of the Association for Computational Linguistics (1986) 247–255.CrossRefGoogle Scholar
  88. 88.
    Milner, R. A theory of type polymorphism in programming. J. Comput. Sys. Sci. 17, pp. 348–375 (1978).MathSciNetMATHCrossRefGoogle Scholar
  89. 89.
    Nadathur, G., A Higher-Order Logic as the Basis for Logic Programming, Ph.D. Dissertation, Department of Computer and Information Science, University of Pennsylvania (1986).Google Scholar
  90. 90.
    Nelson G. and Oppen, D. C. Fast Decision Procedures Based on Congruence Closure. J. ACM 27(2), 356–364, 1980.MathSciNetMATHCrossRefGoogle Scholar
  91. 91.
    Nutt, W., Réty, P., and Smolka, G., “Basic Narrowing Revisited”, Special Issue on Unification, Part I Journal of Symbolic Computation 7(3 & 4), pp. 295–318 (1989).MATHCrossRefGoogle Scholar
  92. 92.
    Paterson, M.S., Wegman, M.N., “Linear Unification”, Journal of Computer and System Sciences, 16 (1978) 158–167.MathSciNetMATHCrossRefGoogle Scholar
  93. 93.
    Paulson, L.C., “Natural Deduction as Higher-Order Resolution”, Journal of Logic Programming 3:3 (1986) 237–258.MathSciNetMATHCrossRefGoogle Scholar
  94. 94.
    Pfenning, F., Proof Transformations in Higher-Order Logic, Ph.D. thesis, Department of Mathematics, Carnegie Mellon University, Pittsburgh, Pa. (1987).Google Scholar
  95. 95.
    Pfenning, F., “Partial Polymorphic Type Inference and Higher-Order Unification”, in Proceedings of the 1988 ACM Conference on Lisp and Functional Programming, ACM, July 1988.Google Scholar
  96. 96.
    Pfenning, F., and Elliott, C, “Higher-Order Abstract Syntax”, Proceedings of the SIGPLAN ’88 Symposium on Language Design and Implementation, ACM, June 1988. 97. Pietrzykowski, T., “A Complete Mechanization of Second-Order Logic”, J ACM 20:2 (1971) 333–364.Google Scholar
  97. 97.
    Pietrzykowski, T.,“A Complete Mechanization of Second-Order Logic,” JACM 20:2 (1971) 333–364.MathSciNetCrossRefGoogle Scholar
  98. 98.
    Pietrzykowski, T., and Jensen, D., “Mechanizing cj-Order Type Theory Through Unification”, TCS 3 (1976) 123–171.MathSciNetCrossRefGoogle Scholar
  99. 98.
    Piotkin, G., “Building in Equational Theories,” Machine Intelligence 7 (1972) 73–90.Google Scholar
  100. 100.
    Rémy, Didier, “Algèbres Touffues. Application au typage polymorphique des objects enregistrements dans les languages fonctionnels”. These, Université Paris VII, 1990.Google Scholar
  101. 101.
    Rémy, Didier, “Records and variants as a natural extension in ML”, Sixteenth ACM Annual Symposium on Principles of Programming Languages, Austin Texas, 1989.Google Scholar
  102. 102.
    Rety, P., “Improving Basic Narrowing Techniques”, Proceedings of the RTA, Bordeaux, Prance (1987).Google Scholar
  103. 103.
    Robinson, J.A., “A Machine Oriented Logic Based on the Resolution Principle”, JACM 12 (1965) 23–41.MATHCrossRefGoogle Scholar
  104. 104.
    Robinson, J.A. , “A Review on Automatic Theorem Proving”, Annual Symposia in Applied Mathematics, 1–18 (1967).Google Scholar
  105. 105.
    Robinson, J.A., “Mechanizing Higher-Order Logic”, Machine Intelligence 4 (1969) 151–170.MATHGoogle Scholar
  106. 106.
    Siekmann, J. H. Unification Theory, Special Issue on Unification, Part I, Journal of Symbolic Computation 7(3 & 4), pp. 207–274 (1989).MathSciNetMATHCrossRefGoogle Scholar
  107. 107.
    Siekmann, J. H., and Szabo, P. Universal unification and classification of equational theories. CADE’82, Lecture Notes in Computer Science, No. 138 (1982).Google Scholar
  108. 108.
    Shieber, S. An Introduction to Unification-Based Approaches to Grammar. CSLI Lecture Notes Series, Center for the study of Language and Information, Stanford, CA (1986).Google Scholar
  109. 109.
    Slagle, J.R., “Automated Theorem Proving for Theories with Simplifiers, Commuta-tivity, and Associativity”, JACM 21 (1974) 622–642.MathSciNetMATHCrossRefGoogle Scholar
  110. 110.
    Schmidt-Schauss, M. Unification in Permutative Equational Theories is Undecidable. Journal of Symbolic Computation 8(4), pp. 415–422 (1989).MathSciNetMATHCrossRefGoogle Scholar
  111. 111.
    Schmidt-Schauss, M. Unification in a Combination of Arbitrary Disjoint Equational Theories. Special issue on Unification, Part II, Journal of Symbolic Computation 8(1 k 2), 51–99 (1989).MathSciNetMATHCrossRefGoogle Scholar
  112. 112.
    Snyder, W. Complete Sets of Transformations for General Unification, Ph.D. thesis. Department of Computer and Information Science, University of Pennsylvania, PA (1988).Google Scholar
  113. 113.
    Snyder, W., and Gallier, J.H., “Higher-Order Unification Revisited: Complete Sets of Transformations”, Special issue on Unification, Part II, Journal of Symbolic Computation 8(1 & 2), 101–140 (1989).MathSciNetMATHCrossRefGoogle Scholar
  114. 114.
    Snyder, W., “Efficient Ground Completion: A Fast Algorithm for Generating Reduced Ground Rewriting Systems from a Set of Ground Equations”, RTA’89, Chapel Hill, NC (journal version submitted for publication).Google Scholar
  115. 115.
    Snyder, W., “Higher-Order E-Unification”, CADE’90, Kaiserslautern, Germany.Google Scholar
  116. 116.
    Snyder, W. The Theory of General Unification. Birkhauser Boston, Inc. (in preparation).Google Scholar
  117. 117.
    Snyder, W., and C. Lynch, “Goal-Directed Strategies for Paramodulation”, Proceedings of the Fourth Conference on Rewrite Techniques and Applications, Como, Italy (1991).Google Scholar
  118. 118.
    Statman, R., “On the Existence of Closed Terms in the Typed A-Calculus II: Transformations of Unification Problems”, TCS 15:3 (1981) 329–338.MathSciNetMATHCrossRefGoogle Scholar
  119. 119.
    Szabo, P. Unifikationstheorie erster Ordnung, Ph.D. thesis, Universität Karlsruhe (1982).Google Scholar
  120. 120.
    Tiden, E., and Arnborg, S. Unification problems with one-sided distributivity. Journal of Symbolic Computation 3(1 & 2), pp. 183–202 (1987).MathSciNetMATHCrossRefGoogle Scholar
  121. 121.
    Winterstein, G., “Unification in Second-Order Logic”, Electronische Informationsverarbeitung und Kybernetik 13 (1977) 399–411.MathSciNetMATHGoogle Scholar
  122. 122.
    Yelick, K. Unification in combinations of collapse-free regular theories. Journal of Symbolic Computation 3(1 & 2), pp. 153–182 (1987).MathSciNetMATHCrossRefGoogle Scholar
  123. 123.
    Zaionc, Marek , “The Set of Unifiers in Typed A-Calculus as a Regular Expression”, Proceedings of the RTA 1985.Google Scholar

Copyright information

© Springer-Verlag New York, Inc 1992

Authors and Affiliations

  • Jean H. Gallier
    • 1
  • Wayne Snyder
    • 2
  1. 1.Computer and Information Science DepartmentUniversity of PennsylvaniaPhiladelphiaUSA
  2. 2.Computer Science DepartmentBoston UniversityBostonUSA

Personalised recommendations