Skip to main content
SpringerLink
Log in

Universal Unification

  • Conference paper
7th International Conference on Automated Deduction (CADE 1984)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 170))

Included in the following conference series:

Abstract

This article surveys what is presently known about first order unification theory.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Bibliography

  1. Barrow, Ambler, Burstall: ‘Some techniques for recognizing Structures in Pictures’, Frontiers of Pattern Recognition, Academic Press Inc., 1972

    Google Scholar 

  2. L.D. Baxter: ‘The Undecidability of the Third Order Dyadic Unification Problem’,, Information and Control, vol.38, no.2, 1978

    Google Scholar 

  3. L.D. Baxter: ‘An efficient Unification Algorithm’, Rep. CS-7323, University of Waterloo, Dept. of analysis and Computer Science, 1973

    Google Scholar 

  4. H. Bryan, J. Carnog: ‘Search methods used with transistor patent applications’, IEEE Spectrum 3, 2, 1966

    Article  Google Scholar 

  5. H.P. Böhm, H.L. Fischer, P. Raulefs: ‘CSSA: Language Concepts and Programming Methodology’, Proc. of ACM, SIGPLAN/ART Conference, Rochester, 1977

    Google Scholar 

  6. F. Blair et al: ‘SCRATCHPAD/1: An interactive facility for symbolic mathematics’, Proc. of the 2nd Symposium on Symbolic Manipulation, Los Angeles, 1971

    Google Scholar 

  7. A. Ballantyne, D. Lankford: ‘Decision Procedures for simple equational theories’, University of Texas at Austin, ATP-35, ATP-37, ATP-39, 1977

    Google Scholar 

  8. R. Boyer, J.S. Moore: ‘A Fast String Searching Algorithm’, CACM vol. 20, no. 10, 1977

    Google Scholar 

  9. D.G. Bobrow (ed): ‘Symbol Manipulation Languages’, Proc. of IFIP, North Holland Publishing Comp., 1968

    Google Scholar 

  10. H. Boley: ‘Directed Recursive Labelnode Bypergraphs: A New Representation Language’, Journal of Artificial Intelligence, vol. 9, no. 1, 1977

    Google Scholar 

  11. Caviness: ‘On Canonical Form and Simplification’, JACM, vol. 17, no. 2, 1970

    Google Scholar 

  12. CODASYL Systems Committee: ‘A survey of Generalized Data Base Management Systems’, Techn.Rep. 1969, ACM and IAG

    Google Scholar 

  13. CODASYL Systems Committee: ‘Feature Analysis of Generalized Data Base Management Systems’, TR 1971, ACM, BC and IAG

    Google Scholar 

  14. Cook: ‘Algebraic techniques and the mechanization of number theory’, RM-4319-PR, Rand Corp., Santa Monica, Cal., 1965

    Google Scholar 

  15. C. Christensen, M. Karr: ‘IAM, A System for interactive algebraic Manipulation’, Proc. of the 2nd Symposium on Symbolic Manipulation, Los Angeles, 1971

    Google Scholar 

  16. M. Clowes: ‘On Seeing Things’, Techn.Rep. 1969, ACM and IAG

    Google Scholar 

  17. W. Clocksin, C. Mellish: ‘Programming in PBOLOG’, Springer 1981

    Google Scholar 

  18. E.F. Codd: ‘A Relational Model of Data for Large shared Databanks’, CACM, 13,6,1972

    Google Scholar 

  19. E.F. Codd: ‘Relational Completeness of Data Base Sublanguages’, in Data Base Systems, Prentice Hall, Courant Comp. Science Symposia Series, vo. 6, 1972

    Google Scholar 

  20. A. Clifford, G. Preston: ‘The Algebraic Theory of Semigroups’, vol.I and vol. II, 1961

    Google Scholar 

  21. D.G. Corneil: ‘Graph Isomorphism’, Ph.D.Dept. of Computer Science, University of Toronto, 1968

    Google Scholar 

  22. J.L. Darlington: ‘A partial Mechanization of Second Order Logic’, Mach.Int. 6, 1971

    Google Scholar 

  23. C.J. Date: ‘An Introduction to Database Systems’, Addison-Wesley Publ. Comp. Inc., 1976

    Google Scholar 

  24. M. Davis: ‘Hilpert’s tenth Problem is unsolvable’, Amer.Math.Monthly, vol. 80, 1973

    Google Scholar 

  25. R. Fateman: ‘The User-Level Semantic Matching Capability in MACSYMA’, Proc. of the 2nd Symposium on Symbolic Manipulation, Los Angeles, 1971

    Google Scholar 

  26. M. Fay: ‘First Order Unification in an Equational Theory’, Proc. 4th Workshop on autom. Deduction, Texas, 1979

    Google Scholar 

  27. F. Fage: ‘Associative Commutative Unification’, INRIA report CNRS-LITP4, 1983 (see also this volume)

    Google Scholar 

  28. D.J. Farber, R.E. Griswald, I.P. Polonsky: ‘SNOBOL as String Manipulation Language’, JACM, vol. 11, no.2, 1964

    Google Scholar 

  29. F. Fage, G. Huet: ‘Complete Sets of Unifiers and Matchers in Equational Theories’, Proc. CAAP-83, Springer Lec.Notes Comp. Sci, vol. 159, 1983

    Google Scholar 

  30. J.F. Gimpel: ‘A Theory of Discrete Patterns and their Implementation in SNOBOL4, CACM 16, 2, 1973

    Article  MathSciNet  Google Scholar 

  31. H. Gallaire, J. Minker. ‘Logic and Databases’, Plenum Press, 1978

    Google Scholar 

  32. W.E. Gould. ‘A matching procedure for ω-order logic’, Scientific report no.4, Air Force Cambridge Research Labs., 1966

    Google Scholar 

  33. J.R. Guard, F.C. Oglesby, J.R. Benneth, L.G. Settle: ‘Semi-Automated Mathematics’, JACM 1969. vol. 18, no.1

    Google Scholar 

  34. D. Goldfarb: ‘The Undecidability of the Second Order Unification Problem’, Journal of Theor. Comp.Sci., 13, 1981

    Google Scholar 

  35. G. Grätzer. ‘Universal Algebra’, Springer Verlag, 1979

    Google Scholar 

  36. W.K. Giloi, J. Siekmann: ‘Entrichtungen von Rechnerarchitekturen für Anwendungen in der Künstlichen Intelligenz’, BMFT-Antrag 1984, Univ. Berlin und Kaiserslautern

    Google Scholar 

  37. J.R. Guard: ‘Automated logic for semi-automated mathematics’, Scientific report no.1, Air Force Cambridge Research Labs., AD 602 710, 1964

    Google Scholar 

  38. A. Herold: ‘Universal Unification and a Class of Equational Theories’, Proc. GWAI-82, W. Wahlster (ed) Springer Fachberichte, 1982

    Google Scholar 

  39. A. Herold: ‘Some Basic Notions of first Order Unification Theory’, Univ. Karlsruhe, Interner Report, 1983

    Google Scholar 

  40. J. Herbrand. ‘Recherches sour la theorle de la demonstration’, Travaux de la Soc. des Sciences et des Lettre de Varsovle, no.33, 128, 1930

    Google Scholar 

  41. G.P. Huet: ‘A Unification Algorithm for typed λ-Calculus’, J.Theor. Comp. Sci., 1, 1975

    Google Scholar 

  42. J.I. Hmelevskij: ‘The solution of certain systems of word equations’, Dokl.Akad. Nauk SSSR, 1964, 749 Soviet Math. Dokl.5, 1964, 724

    Google Scholar 

  43. J.I. Hmelevskij: ‘Word equations without coefficients’, Dokl. Acad. Nauk. SSSR 171, 1966, 1047 Soviet Math. Dokl. 7, 1966, 1611

    MathSciNet  Google Scholar 

  44. J.I. Hmelevskij: ‘Solution of word equations in three unknowns’, Dokl. Akad. Nauk. SSR 177, 1967, no.5, Soviet Math. Dokl. 8, 1967, no. 6

    Google Scholar 

  45. J.M. Hullot: ‘A Catalogue of Canonical Term Rewriting Systems, Research Rep. CSL-113, SRI-International, 1980

    Google Scholar 

  46. A. Hearn: ‘REDUCE2, A System and Language for Algebraic Manipulation’, Proc. of the 2nd Symposium on Symbolic Manipulation, Los Angeles, 1971

    Google Scholar 

  47. J. Howle: ‘Introduction to Semigroup Theory’, Acad. Press 1976

    Google Scholar 

  48. G. Huet, D.C. Oppen: ‘Equations and Rewrite Rules’, in ‘Formal Languages: Perspectlves and Open Problems’, Ed. R. Book, Academic Press, 1980

    Google Scholar 

  49. S. Heilbrunner: ‘Gleichungssysteme für Zeichenreihen’, TU München, Abtl. Mathematik, Ber.Nr. 7311,1973

    Google Scholar 

  50. C. Hewitt: ‘Description and Theoretlcal analysis of PLANNER a language for proving theorems and manipulating models in a robot’, Dept. of Mathematics, Ph.C. Thesis, MIT, 1972

    Google Scholar 

  51. C. Hewitt. ‘Viewing Control Structures as Patterns of Passing Massages’, MIT, AI-Lab., Working paper 92, 1976

    Google Scholar 

  52. G. P. Huet. ‘Constrained resolution: a complete method for theory’, Jenning’s Computing Centre rep. 1117, Case Western Reserve Univ., 1972

    Google Scholar 

  53. G.P. Huet: ‘The undecidability of unification in third order logic’, Information and Control 22(3), 257–267, 1973

    Article  MathSciNet  MATH  Google Scholar 

  54. G. Huet: ‘Unification in typed Lambda Calculus’, in λ-Calculus and Comp. Sci. Theory, Springer Lecture Notes, No.37, Proc. of the Symp. held in Rome, 1975

    Google Scholar 

  55. G. Huet: ‘Resolution d’equations dans des langauges d’ordere 1,2,..,ω’, These d’Etat, Univ. de Paris, VII, 1976

    Google Scholar 

  56. G. Huet: ‘An Algorithm to Generate the Basis of Solutions to Homogenous Linear Diophantine Equations’, Information Proc. letters 7,3, 1978

    Google Scholar 

  57. G. Huet: ‘Confluent reductions: Abstract Properties and Applications to Term Rewriting Systems’, JACM vo. 27, no.4, 1980

    Google Scholar 

  58. J.M. Hullot: ‘Associative Commutative Pattern Matching’, 5th Int.Joint Conf. on AI, Tokyo 1979

    Google Scholar 

  59. J.M. Hullot: ‘Canonical Forms and Unification’, Proc. of 5th Workshop on Automated Deduction’, Springer Lecture Notes, 1980

    Google Scholar 

  60. D. Jensen, T. Pietrzykowski: ‘Mechanising λ-order type theory through unification’, Rep. CS73-16, Dept. of Applied Analysis and Comp. 4, 1972

    Google Scholar 

  61. J. Jouannaud, C. Kirchner, H. Kirchner: ‘Incremental Unification in Equational Theories’, Université de Nancy, Informatique, 82-R-047, 1982

    Google Scholar 

  62. D. E. Knuth, P.B. Bendix: ‘Simple word Problems in Universal Algebras’, in: Computational Problems in Abstract Algebra, J. Leech (ed), Pergamon Press, Oxford, 1970

    Google Scholar 

  63. D. Kapur, M.S. Krishnamoorthy, P. Narendran: ‘A new linear Algorithm for Unification’, General Electric, Rep. no. 82CRD-100, New York, 1982

    Google Scholar 

  64. Karp, Miller, Rosenberg: ‘Rapid Identification of repeated Patterns in Strings, Trees and Arrays’, ACM Symposium on Th.of Comp. 4, 1972

    Google Scholar 

  65. Knuth, Morris, Pratt: ‘Fast Pattern Matching in Strings’, Stan-CS-74-440, Stanford University, Comp. Sci. Dept., 1974

    Google Scholar 

  66. S. Kühner, Ch. Mathis, P. Raulefs, J. Siekmann: ‘Unification of Idempotent Functions’, Proceedings of 4th IJCAI, MIT, Cambridge, 1977

    Google Scholar 

  67. R. Kowalski: ‘Logic for Problem Solving’, North Holland, 1979

    Google Scholar 

  68. D.S. Lankford: ‘A Unification Algorithm for Abelian Group Theory’, Rep. MTP-1, Louisiana Techn. Univ., 1979

    Google Scholar 

  69. D.S. Lankford: ‘A new complete FPA-Unification Algorithm’, MIT-8, Louisiana Techn. Univ., 1980

    Google Scholar 

  70. D.S. Lankford, M. Ballantyne: ‘The Refutation Completeness of Blocked Permutative Narrowing and Resolution’, 4th Workshop on Autom. Deduction, Texas, 1979

    Google Scholar 

  71. D. S. Lankford, G. Butler, B. Brady: ‘Abelian Group Unification Algorithms for elementary terms’, to appear in: Contempory Mathematics.

    Google Scholar 

  72. C.L. Lucchesi: ‘The undecidability of the unification problem for third order languages’, Rep. CSRR 2059, Dept. of Applied Analysis and Comp. Science, Univ. of Waterloo, 1972

    Google Scholar 

  73. D. Loveland: ‘Automated Theorem Proving’, North Holland, 1980

    Google Scholar 

  74. M. Livesey, J. Siekmann: ‘Termination and Decidability Results for Stringunification’, Univ. of Essex, Memo CSM-12, 1975

    Google Scholar 

  75. M. Livesey, J. Siekmann: ‘Unification of Sets and Multisets’, Univ. Karlsurhe, Techn.Report, 1976

    Google Scholar 

  76. M. Livesey, J. Siekmann, P. Szabo, E. Unvericht: ‘Unification Problems for Combinations of Associativity, Commutativity, Distributivity and Indempotence Axioms’, Proc. of Conf. on Autom. Deduction, Austin, Texas, 1979

    Google Scholar 

  77. G. Levi, F. Sirovich: ‘Pattern Matching and Goal directed Computation’, Nota Interna B73-12, Univ. of Pisa, 1973

    Google Scholar 

  78. A.A. Markov: ‘Trudy Mat.Inst.Steklov’, no.42, Izdat.Akad. Nauk SSSR, 1954, NR17, 1038, 1954

    Google Scholar 

  79. Y. Matiyasevich: ‘Diophantine Representation of Rec. Enumerable Predicates’, Proc. of the Scand. Logic Symp., North Holland, 1978

    Google Scholar 

  80. G.S. Makanin: ‘The Problem of Solvability of Equations in a Free Semigroup’, Soviet Akad, Nauk SSSR, Tom 233, no.2, 1977

    Google Scholar 

  81. Maurer: ‘Graphs as Strings’, Universität Karlsruhe, Techn. Rep., 1977

    Google Scholar 

  82. Manove, Bloom, Engelmann: ‘Rational Functions in MATHLAB’, IFIP Conf. on Symb. Manipulation, Pisa, 1968

    Google Scholar 

  83. A. Martelli, U. Montaneri: ‘An Efficient Unification Algorithm’, University off Pisa, Techn. Report, 1979

    Google Scholar 

  84. J. Moses: ‘Symbolic Integration: The Stormy Decade’, CACM 14, 8, 1971

    MathSciNet  MATH  Google Scholar 

  85. J. Moses: ‘MACSYMA — the fifth Year’, Project MAC, MIT, Cambridge, 1974

    Google Scholar 

  86. A. Nevins: ‘A Human oriented logic for ATP’, JACM 21, 1974 (first report 1971)

    Google Scholar 

  87. N. Nilsson: ‘Principles of Artificial Intelligence’, Tioga Publ. Comp.,Cal., 1980

    Google Scholar 

  88. G. Nelson, D. Oppen: ‘Fast Decision Procedures Based on Congruence Closure’, JACM, 27, 2, 1980

    Article  MathSciNet  MATH  Google Scholar 

  89. G. Plotkin: ‘Building in Equational Theories’, Machine Intelligence, vol. 7, 1972

    Google Scholar 

  90. D. Prawitz: ‘An Improved Proof Procedure’, Theoria 26, 1960

    Google Scholar 

  91. G. Peterson, M. Stickel: ‘Complete Sets of Reductions for Equational Theories with Complete Unification Algorithms’, JACM, vol, 28, no.2, 1981

    Google Scholar 

  92. M. Paterson, M. Wegman: ‘Linear Unification’, J. of Comp. and Syst. Science, 1968, 16

    Google Scholar 

  93. Rulifson, Derksen, Waldinger: ‘QA4: A procedural calculus for intuitive reasoning’, Stanford Univ., Nov. 1972

    Google Scholar 

  94. J. Rastall: ‘Graph-family Matching’, University of Edinburgh, MIP-R-62, 1969

    Google Scholar 

  95. J.A. Robinson: ‘A review on automatic theorem proving’, Symp. Appl.Math., vol. 19, 1–18, 1967

    Article  MathSciNet  Google Scholar 

  96. J.A. Robinson: ‘A Machine Oriented Logic based on the Resolution Principle’, JACM 12, 1965

    Google Scholar 

  97. J.A. Robinson: ‘Computational Logic: The Unification Computation’, Machine Intelligence, vol. 6, 1971

    Google Scholar 

  98. P. Raulefs, J. Siekmann: ‘Unification of Idempotent Functions’, Universität Karlsruhe, Techn. Report, 1978

    Google Scholar 

  99. P. Raulefs, J. Siekmann, P. Szabo, E. Unvericht: ‘A short Survey on the State of the Art in Matching and Unification Problems, SIGSAM Bulletin, 13, 1979

    Google Scholar 

  100. P. Szabo: ‘Undecidability of the DA-Unification Problem’, Proc. of GWAI, 1979

    Google Scholar 

  101. J. Siekmann, P. Szabo: ‘A Minimal Unification Algorithm for Idempotent Functions’, Universität Karlsruhe, 1982

    Google Scholar 

  102. E.H. Shortliffe: ‘MYCIN: Computer Based Medical Consultations’, North Holland Publ. Comp. 1976

    Google Scholar 

  103. B.C. Smith, C. Hewitt: ‘A Plasma Primer’, MIT, AI-Lab., 1975

    Google Scholar 

  104. R. Shostak: ‘Deciding Combinations of Theories’, JACM, vol. 31, no.1, 1984

    Google Scholar 

  105. SIGSAM Bulletin: ‘ACM special interest group on Symbolic and Algebraic Manipulation, vol. 11, no.3, 1977 (issue no. 43) contains an almost complete bibliography

    Google Scholar 

  106. J. Siekmann: ‘Stringunification’ Essex University, Memo CSM-7, 1975

    Google Scholar 

  107. J. Siekmann: ‘Unification of Commutative Terms’, Uni. Karlsruhe, 1976

    Google Scholar 

  108. J. Siekmann: ‘Unification and Matching Problems’, Ph.D., Essex Univ.,, Memo CSA-4-78

    Google Scholar 

  109. J. R. Slagle: ‘ATP with built-in theories including equality, partial ordering and sets’, JACM 19, 120–135, 1972

    Article  MathSciNet  MATH  Google Scholar 

  110. J. Slagle: ‘ATP for Theories with Simplifiers, Commutativity and Associativity’, JACM 21, 1974

    Google Scholar 

  111. J. Siekmann, P. Szabo: ‘Universal Unification and a Classification of Eqautional Theories’, Proc. of Conf. on Autom. Deduction, 1982, New York, Springer Lecture Notes comp. Sci., vol. 87

    Google Scholar 

  112. J. Siekmann, P. Szabo: ‘Universal Unification and Regular ACFM Theories’, Proc. IJCAI-81, Vancouver, 1981

    Google Scholar 

  113. J. Siekmann, P. Szabo: ‘A Noetherian and Confluent Rewrite System for Indempotent Semigroups’, Semigroup Forum, vol. 25, 1982

    Google Scholar 

  114. D. Skordew, B. Sendow: ‘Z. Math. Logic Grundlagen’, Math.7 (1961), 289, MR 31, 57 (Russian) (English translation at Univ. of Essex, Comp. Sci. Dept.)

    Google Scholar 

  115. M. Stickel: ‘A Unification Algorithm for Assoc. Commutative Functions’, JACM, vol. 28, no.3, 1981

    Google Scholar 

  116. G.F. Stewart: ‘An Algebraic Model for String Patterns’, Univ. of Toronto, CSRG-39, 1974

    Google Scholar 

  117. E. Sussenguth: ‘A graph-theoretical algorithm for matching chemical structures’, J. Chem. Doc. 5, 1, 1965

    Article  Google Scholar 

  118. P. Szabo, E. Unvericht: ‘The Unification Problem for Distributive Terms’, Univ. Karlsruhe, 1978

    Google Scholar 

  119. P. Szabo: ‘Theory of First Order Unification’ (in German, thesis) Univ. Karlsruhe, 1982

    Google Scholar 

  120. A. Tarski: ‘Equational Logic and Equational Theories of Algebra’, Schmidt et al (eds), Contributions to Mathematical Logic, North Holland, 1968

    Google Scholar 

  121. H. Tennant. ‘Natural Language Processing’, Petrocelli Books, 1981

    Google Scholar 

  122. W. Taylor: ‘Equational Logic’, Colloquia Mathematica Societatis Janos Bolya, 1975

    Google Scholar 

  123. J.R. Ullman: ‘An Algorithm for Subgraph Isomorphism’, JACM, vol. 23, no.1, 1976

    Google Scholar 

  124. S.H. Unger: ‘CIT — Heuristic Program for Testing Pairs of directed Line Graphs for Isomorphism’, CACM, vol.7, no.1, 1964

    Google Scholar 

  125. J. van Vaalen: ‘An Extension of Unification to Substitutions with an Application to ATP’, Proc. of Fourth IJCAI, Tbilisi, USSR, 1975

    Google Scholar 

  126. E. Vogel: ‘Unifikation von Morphismen’, Diplomarbeit, Univ. Karlsruhe, 1978

    Google Scholar 

  127. M. Venturini-Zilli: ‘Complexity of the Unification Algorithm for First Order Expression’, Calcolo XII, Easc IV, 1975

    Google Scholar 

  128. D.H.D. Warren: ‘Implementing PROLOG’, vol. 1 and vol. 2, D.A.I. Research Rep., no. 39, Univ. of Edinburgh, 1977

    Google Scholar 

  129. Ch. Walther: ‘Unification in Many Sorted Theories’, Univ. Karlsruhe, 1984

    Google Scholar 

  130. K. Wong, K. Chandra: ‘Bounds for the String Editing Problem’, JACM, vol. 23, no.1, 1976

    Google Scholar 

  131. P. Weiner: ‘Linear Pattern Matching Algorithms’, IEEE Symp. on SW. and Automata Theory, 14, 19773

    Google Scholar 

  132. N. Whitehead: ‘Treatise on Universal Algebra’, 1898

    Google Scholar 

  133. van Wijngaarden (et all): ‘Revised Rep. on the Algorithmic Language ALGOL68’, Springer-Verlag, Berlin, Heidelberg, N.Y., 1976

    Google Scholar 

  134. Winston: ‘The Psychology of Computer Vision’, McGraw Hill, 1975

    Google Scholar 

  135. G. Winterstein: ‘Unification in Second Order Logic’, Bericht 3, Univ. Kaiserslautern, 1976

    Google Scholar 

  136. L. Wos, G.A. Robinson, D. Carson, L. Shalla: ‘The Concept of Demodulation in Theorem Proving’, JACM, vol. 14, no.4, 1967

    Google Scholar 

  137. L. Wos, G. Robinson: ‘Maximal Models and Refutation Completeness: Semidecision Procedures in Automatic Theorem Proving’, in: Word problems (W.W. Boone, F.B. Cannonito, B.C. Lyndon, eds), North Holland, 1973

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. FB Informatik, Universität Kaiserslautern, Postfach 3049, D-6750, Kaiserslautern

    Jörg H. Siekmann

Authors
  1. Jörg H. Siekmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. SRI International, 333 Ravenswood Avenue, Menlo Park, CA, 94025, USA

    R. E. Shostak

Rights and permissions

Reprints and permissions

Copyright information

© 1984 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Siekmann, J.H. (1984). Universal Unification. In: Shostak, R.E. (eds) 7th International Conference on Automated Deduction. CADE 1984. Lecture Notes in Computer Science, vol 170. Springer, New York, NY. https://doi.org/10.1007/978-0-387-34768-4_1

Download citation

  • DOI: https://doi.org/10.1007/978-0-387-34768-4_1

  • Publisher Name: Springer, New York, NY

  • Print ISBN: 978-0-387-96022-7

  • Online ISBN: 978-0-387-34768-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation