Advertisement

Abstract

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

Keywords

Equational Theory Unification Algorithm Automatic Theorem Prover Unification Problem Word Equation 
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.

Bibliography

  1. [BA72]
    Barrow, Ambler, Burstall: ‘Some techniques for recognizing Structures in Pictures’, Frontiers of Pattern Recognition, Academic Press Inc., 1972Google Scholar
  2. [BA78]
    L.D. Baxter: ‘The Undecidability of the Third Order Dyadic Unification Problem’,, Information and Control, vol.38, no.2, 1978Google Scholar
  3. [RA73]
    L.D. Baxter: ‘An efficient Unification Algorithm’, Rep. CS-7323, University of Waterloo, Dept. of analysis and Computer Science, 1973Google Scholar
  4. [BC66]
    H. Bryan, J. Carnog: ‘Search methods used with transistor patent applications’, IEEE Spectrum 3, 2, 1966CrossRefGoogle Scholar
  5. [BF77]
    H.P. Böhm, H.L. Fischer, P. Raulefs: ‘CSSA: Language Concepts and Programming Methodology’, Proc. of ACM, SIGPLAN/ART Conference, Rochester, 1977Google Scholar
  6. [BL71]
    F. Blair et al: ‘SCRATCHPAD/1: An interactive facility for symbolic mathematics’, Proc. of the 2nd Symposium on Symbolic Manipulation, Los Angeles, 1971Google Scholar
  7. [BL77]
    A. Ballantyne, D. Lankford: ‘Decision Procedures for simple equational theories’, University of Texas at Austin, ATP-35, ATP-37, ATP-39, 1977Google Scholar
  8. [BM77]
    R. Boyer, J.S. Moore: ‘A Fast String Searching Algorithm’, CACM vol. 20, no. 10, 1977Google Scholar
  9. [B068]
    D.G. Bobrow (ed): ‘Symbol Manipulation Languages’, Proc. of IFIP, North Holland Publishing Comp., 1968Google Scholar
  10. [BO77]
    H. Boley: ‘Directed Recursive Labelnode Bypergraphs: A New Representation Language’, Journal of Artificial Intelligence, vol. 9, no. 1, 1977Google Scholar
  11. [CA70]
    Caviness: ‘On Canonical Form and Simplification’, JACM, vol. 17, no. 2, 1970Google Scholar
  12. [CD69]
    CODASYL Systems Committee: ‘A survey of Generalized Data Base Management Systems’, Techn.Rep. 1969, ACM and IAGGoogle Scholar
  13. [CD71]
    CODASYL Systems Committee: ‘Feature Analysis of Generalized Data Base Management Systems’, TR 1971, ACM, BC and IAGGoogle Scholar
  14. [CK67]
    Cook: ‘Algebraic techniques and the mechanization of number theory’, RM-4319-PR, Rand Corp., Santa Monica, Cal., 1965Google Scholar
  15. [CK71]
    C. Christensen, M. Karr: ‘IAM, A System for interactive algebraic Manipulation’, Proc. of the 2nd Symposium on Symbolic Manipulation, Los Angeles, 1971Google Scholar
  16. [CL71]
    M. Clowes: ‘On Seeing Things’, Techn.Rep. 1969, ACM and IAGGoogle Scholar
  17. [CM81]
    W. Clocksin, C. Mellish: ‘Programming in PBOLOG’, Springer 1981Google Scholar
  18. [CO70]
    E.F. Codd: ‘A Relational Model of Data for Large shared Databanks’, CACM, 13,6,1972Google Scholar
  19. [CO72]
    E.F. Codd: ‘Relational Completeness of Data Base Sublanguages’, in Data Base Systems, Prentice Hall, Courant Comp. Science Symposia Series, vo. 6, 1972Google Scholar
  20. [CP61]
    A. Clifford, G. Preston: ‘The Algebraic Theory of Semigroups’, vol.I and vol. II, 1961Google Scholar
  21. [CR68]
    D.G. Corneil: ‘Graph Isomorphism’, Ph.D.Dept. of Computer Science, University of Toronto, 1968Google Scholar
  22. [DA71]
    J.L. Darlington: ‘A partial Mechanization of Second Order Logic’, Mach.Int. 6, 1971Google Scholar
  23. [DA76]
    C.J. Date: ‘An Introduction to Database Systems’, Addison-Wesley Publ. Comp. Inc., 1976Google Scholar
  24. [DA73]
    M. Davis: ‘Hilpert’s tenth Problem is unsolvable’, Amer.Math.Monthly, vol. 80, 1973Google Scholar
  25. [FA71]
    R. Fateman: ‘The User-Level Semantic Matching Capability in MACSYMA’, Proc. of the 2nd Symposium on Symbolic Manipulation, Los Angeles, 1971Google Scholar
  26. [FA79]
    M. Fay: ‘First Order Unification in an Equational Theory’, Proc. 4th Workshop on autom. Deduction, Texas, 1979Google Scholar
  27. [FA83]
    F. Fage: ‘Associative Commutative Unification’, INRIA report CNRS-LITP4, 1983 (see also this volume)Google Scholar
  28. [FG64]
    D.J. Farber, R.E. Griswald, I.P. Polonsky: ‘SNOBOL as String Manipulation Language’, JACM, vol. 11, no.2, 1964Google Scholar
  29. [FH83]
    F. Fage, G. Huet: ‘Complete Sets of Unifiers and Matchers in Equational Theories’, Proc. CAAP-83, Springer Lec.Notes Comp. Sci, vol. 159, 1983Google Scholar
  30. [GI73]
    J.F. Gimpel: ‘A Theory of Discrete Patterns and their Implementation in SNOBOL4, CACM 16, 2, 1973MathSciNetCrossRefGoogle Scholar
  31. [GM78]
    H. Gallaire, J. Minker. ‘Logic and Databases’, Plenum Press, 1978Google Scholar
  32. [GO66]
    W.E. Gould. ‘A matching procedure for ω-order logic’, Scientific report no.4, Air Force Cambridge Research Labs., 1966Google Scholar
  33. [GO67]
    J.R. Guard, F.C. Oglesby, J.R. Benneth, L.G. Settle: ‘Semi-Automated Mathematics’, JACM 1969. vol. 18, no.1Google Scholar
  34. [GO81]
    D. Goldfarb: ‘The Undecidability of the Second Order Unification Problem’, Journal of Theor. Comp.Sci., 13, 1981Google Scholar
  35. [GR79]
    G. Grätzer. ‘Universal Algebra’, Springer Verlag, 1979Google Scholar
  36. [GS84]
    W.K. Giloi, J. Siekmann: ‘Entrichtungen von Rechnerarchitekturen für Anwendungen in der Künstlichen Intelligenz’, BMFT-Antrag 1984, Univ. Berlin und KaiserslauternGoogle Scholar
  37. [GU64]
    J.R. Guard: ‘Automated logic for semi-automated mathematics’, Scientific report no.1, Air Force Cambridge Research Labs., AD 602 710, 1964Google Scholar
  38. [HD82]
    A. Herold: ‘Universal Unification and a Class of Equational Theories’, Proc. GWAI-82, W. Wahlster (ed) Springer Fachberichte, 1982Google Scholar
  39. [HE82]
    A. Herold: ‘Some Basic Notions of first Order Unification Theory’, Univ. Karlsruhe, Interner Report, 1983Google Scholar
  40. [HE30]
    J. Herbrand. ‘Recherches sour la theorle de la demonstration’, Travaux de la Soc. des Sciences et des Lettre de Varsovle, no.33, 128, 1930Google Scholar
  41. [HE75]
    G.P. Huet: ‘A Unification Algorithm for typed λ-Calculus’, J.Theor. Comp. Sci., 1, 1975Google Scholar
  42. [HJ64]
    J.I. Hmelevskij: ‘The solution of certain systems of word equations’, Dokl.Akad. Nauk SSSR, 1964, 749 Soviet Math. Dokl.5, 1964, 724Google Scholar
  43. [HJ66]
    J.I. Hmelevskij: ‘Word equations without coefficients’, Dokl. Acad. Nauk. SSSR 171, 1966, 1047 Soviet Math. Dokl. 7, 1966, 1611MathSciNetGoogle Scholar
  44. [HJ67]
    J.I. Hmelevskij: ‘Solution of word equations in three unknowns’, Dokl. Akad. Nauk. SSR 177, 1967, no.5, Soviet Math. Dokl. 8, 1967, no. 6Google Scholar
  45. [HL80]
    J.M. Hullot: ‘A Catalogue of Canonical Term Rewriting Systems, Research Rep. CSL-113, SRI-International, 1980Google Scholar
  46. [HNT1]
    A. Hearn: ‘REDUCE2, A System and Language for Algebraic Manipulation’, Proc. of the 2nd Symposium on Symbolic Manipulation, Los Angeles, 1971Google Scholar
  47. [HO76]
    J. Howle: ‘Introduction to Semigroup Theory’, Acad. Press 1976Google Scholar
  48. [HO80]
    G. Huet, D.C. Oppen: ‘Equations and Rewrite Rules’, in ‘Formal Languages: Perspectlves and Open Problems’, Ed. R. Book, Academic Press, 1980Google Scholar
  49. [HR73]
    S. Heilbrunner: ‘Gleichungssysteme für Zeichenreihen’, TU München, Abtl. Mathematik, Ber.Nr. 7311,1973Google Scholar
  50. [HT72]
    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, 1972Google Scholar
  51. [HT76]
    C. Hewitt. ‘Viewing Control Structures as Patterns of Passing Massages’, MIT, AI-Lab., Working paper 92, 1976Google Scholar
  52. [HT72]
    G. P. Huet. ‘Constrained resolution: a complete method for theory’, Jenning’s Computing Centre rep. 1117, Case Western Reserve Univ., 1972Google Scholar
  53. [HT73]
    G.P. Huet: ‘The undecidability of unification in third order logic’, Information and Control 22(3), 257–267, 1973MathSciNetCrossRefzbMATHGoogle Scholar
  54. [HT75]
    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, 1975Google Scholar
  55. [HT76]
    G. Huet: ‘Resolution d’equations dans des langauges d’ordere 1,2,..,ω’, These d’Etat, Univ. de Paris, VII, 1976Google Scholar
  56. [HT78]
    G. Huet: ‘An Algorithm to Generate the Basis of Solutions to Homogenous Linear Diophantine Equations’, Information Proc. letters 7,3, 1978Google Scholar
  57. [HT80]
    G. Huet: ‘Confluent reductions: Abstract Properties and Applications to Term Rewriting Systems’, JACM vo. 27, no.4, 1980Google Scholar
  58. [HU79]
    J.M. Hullot: ‘Associative Commutative Pattern Matching’, 5th Int.Joint Conf. on AI, Tokyo 1979Google Scholar
  59. [HU80]
    J.M. Hullot: ‘Canonical Forms and Unification’, Proc. of 5th Workshop on Automated Deduction’, Springer Lecture Notes, 1980Google Scholar
  60. [JP73]
    D. Jensen, T. Pietrzykowski: ‘Mechanising λ-order type theory through unification’, Rep. CS73-16, Dept. of Applied Analysis and Comp. 4, 1972Google Scholar
  61. [JKK82]
    J. Jouannaud, C. Kirchner, H. Kirchner: ‘Incremental Unification in Equational Theories’, Université de Nancy, Informatique, 82-R-047, 1982Google Scholar
  62. [KB70]
    D. E. Knuth, P.B. Bendix: ‘Simple word Problems in Universal Algebras’, in: Computational Problems in Abstract Algebra, J. Leech (ed), Pergamon Press, Oxford, 1970Google Scholar
  63. [KK82]
    D. Kapur, M.S. Krishnamoorthy, P. Narendran: ‘A new linear Algorithm for Unification’, General Electric, Rep. no. 82CRD-100, New York, 1982Google Scholar
  64. [KM72]
    Karp, Miller, Rosenberg: ‘Rapid Identification of repeated Patterns in Strings, Trees and Arrays’, ACM Symposium on Th.of Comp. 4, 1972Google Scholar
  65. [KM74]
    Knuth, Morris, Pratt: ‘Fast Pattern Matching in Strings’, Stan-CS-74-440, Stanford University, Comp. Sci. Dept., 1974Google Scholar
  66. [KM77]
    S. Kühner, Ch. Mathis, P. Raulefs, J. Siekmann: ‘Unification of Idempotent Functions’, Proceedings of 4th IJCAI, MIT, Cambridge, 1977Google Scholar
  67. [KO79]
    R. Kowalski: ‘Logic for Problem Solving’, North Holland, 1979Google Scholar
  68. [LA79]
    D.S. Lankford: ‘A Unification Algorithm for Abelian Group Theory’, Rep. MTP-1, Louisiana Techn. Univ., 1979Google Scholar
  69. [LA80]
    D.S. Lankford: ‘A new complete FPA-Unification Algorithm’, MIT-8, Louisiana Techn. Univ., 1980Google Scholar
  70. [LB79]
    D.S. Lankford, M. Ballantyne: ‘The Refutation Completeness of Blocked Permutative Narrowing and Resolution’, 4th Workshop on Autom. Deduction, Texas, 1979Google Scholar
  71. [LBB84]
    D. S. Lankford, G. Butler, B. Brady: ‘Abelian Group Unification Algorithms for elementary terms’, to appear in: Contempory Mathematics.Google Scholar
  72. [LC72]
    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, 1972Google Scholar
  73. [LO80]
    D. Loveland: ‘Automated Theorem Proving’, North Holland, 1980Google Scholar
  74. [LS75]
    M. Livesey, J. Siekmann: ‘Termination and Decidability Results for Stringunification’, Univ. of Essex, Memo CSM-12, 1975Google Scholar
  75. [LS76]
    M. Livesey, J. Siekmann: ‘Unification of Sets and Multisets’, Univ. Karlsurhe, Techn.Report, 1976Google Scholar
  76. [LS79]
    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, 1979Google Scholar
  77. [LS73]
    G. Levi, F. Sirovich: ‘Pattern Matching and Goal directed Computation’, Nota Interna B73-12, Univ. of Pisa, 1973Google Scholar
  78. [MA54]
    A.A. Markov: ‘Trudy Mat.Inst.Steklov’, no.42, Izdat.Akad. Nauk SSSR, 1954, NR17, 1038, 1954Google Scholar
  79. [MA70]
    Y. Matiyasevich: ‘Diophantine Representation of Rec. Enumerable Predicates’, Proc. of the Scand. Logic Symp., North Holland, 1978Google Scholar
  80. [MA77]
    G.S. Makanin: ‘The Problem of Solvability of Equations in a Free Semigroup’, Soviet Akad, Nauk SSSR, Tom 233, no.2, 1977Google Scholar
  81. [MA77]
    Maurer: ‘Graphs as Strings’, Universität Karlsruhe, Techn. Rep., 1977Google Scholar
  82. [MB68]
    Manove, Bloom, Engelmann: ‘Rational Functions in MATHLAB’, IFIP Conf. on Symb. Manipulation, Pisa, 1968Google Scholar
  83. [MM79]
    A. Martelli, U. Montaneri: ‘An Efficient Unification Algorithm’, University off Pisa, Techn. Report, 1979Google Scholar
  84. [MO71]
    J. Moses: ‘Symbolic Integration: The Stormy Decade’, CACM 14, 8, 1971MathSciNetzbMATHGoogle Scholar
  85. [MO74]
    J. Moses: ‘MACSYMA — the fifth Year’, Project MAC, MIT, Cambridge, 1974Google Scholar
  86. [NE71]
    A. Nevins: ‘A Human oriented logic for ATP’, JACM 21, 1974 (first report 1971)Google Scholar
  87. [NI80]
    N. Nilsson: ‘Principles of Artificial Intelligence’, Tioga Publ. Comp.,Cal., 1980Google Scholar
  88. [NO80]
    G. Nelson, D. Oppen: ‘Fast Decision Procedures Based on Congruence Closure’, JACM, 27, 2, 1980MathSciNetCrossRefzbMATHGoogle Scholar
  89. [PL72]
    G. Plotkin: ‘Building in Equational Theories’, Machine Intelligence, vol. 7, 1972Google Scholar
  90. [PR60]
    D. Prawitz: ‘An Improved Proof Procedure’, Theoria 26, 1960Google Scholar
  91. [PS81]
    G. Peterson, M. Stickel: ‘Complete Sets of Reductions for Equational Theories with Complete Unification Algorithms’, JACM, vol, 28, no.2, 1981Google Scholar
  92. [PW78]
    M. Paterson, M. Wegman: ‘Linear Unification’, J. of Comp. and Syst. Science, 1968, 16Google Scholar
  93. [RD72]
    Rulifson, Derksen, Waldinger: ‘QA4: A procedural calculus for intuitive reasoning’, Stanford Univ., Nov. 1972Google Scholar
  94. [RL69]
    J. Rastall: ‘Graph-family Matching’, University of Edinburgh, MIP-R-62, 1969Google Scholar
  95. [RN67]
    J.A. Robinson: ‘A review on automatic theorem proving’, Symp. Appl.Math., vol. 19, 1–18, 1967MathSciNetCrossRefGoogle Scholar
  96. [RO65]
    J.A. Robinson: ‘A Machine Oriented Logic based on the Resolution Principle’, JACM 12, 1965Google Scholar
  97. [RO71]
    J.A. Robinson: ‘Computational Logic: The Unification Computation’, Machine Intelligence, vol. 6, 1971Google Scholar
  98. [RS78]
    P. Raulefs, J. Siekmann: ‘Unification of Idempotent Functions’, Universität Karlsruhe, Techn. Report, 1978Google Scholar
  99. [RSS79]
    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, 1979Google Scholar
  100. [SB82]
    P. Szabo: ‘Undecidability of the DA-Unification Problem’, Proc. of GWAI, 1979Google Scholar
  101. [SB82]
    J. Siekmann, P. Szabo: ‘A Minimal Unification Algorithm for Idempotent Functions’, Universität Karlsruhe, 1982Google Scholar
  102. [SH76]
    E.H. Shortliffe: ‘MYCIN: Computer Based Medical Consultations’, North Holland Publ. Comp. 1976Google Scholar
  103. [SH75]
    B.C. Smith, C. Hewitt: ‘A Plasma Primer’, MIT, AI-Lab., 1975Google Scholar
  104. [SH84]
    R. Shostak: ‘Deciding Combinations of Theories’, JACM, vol. 31, no.1, 1984Google Scholar
  105. [SG77]
    SIGSAM Bulletin: ‘ACM special interest group on Symbolic and Algebraic Manipulation, vol. 11, no.3, 1977 (issue no. 43) contains an almost complete bibliographyGoogle Scholar
  106. [S175]
    J. Siekmann: ‘Stringunification’ Essex University, Memo CSM-7, 1975Google Scholar
  107. [SI76]
    J. Siekmann: ‘Unification of Commutative Terms’, Uni. Karlsruhe, 1976Google Scholar
  108. [S178]
    J. Siekmann: ‘Unification and Matching Problems’, Ph.D., Essex Univ.,, Memo CSA-4-78Google Scholar
  109. [SL72]
    J. R. Slagle: ‘ATP with built-in theories including equality, partial ordering and sets’, JACM 19, 120–135, 1972MathSciNetCrossRefzbMATHGoogle Scholar
  110. [SL74]
    J. Slagle: ‘ATP for Theories with Simplifiers, Commutativity and Associativity’, JACM 21, 1974Google Scholar
  111. [SO82]
    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. 87Google Scholar
  112. [SS81]
    J. Siekmann, P. Szabo: ‘Universal Unification and Regular ACFM Theories’, Proc. IJCAI-81, Vancouver, 1981Google Scholar
  113. [SS82]
    J. Siekmann, P. Szabo: ‘A Noetherian and Confluent Rewrite System for Indempotent Semigroups’, Semigroup Forum, vol. 25, 1982Google Scholar
  114. [SS61]
    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. [ST81]
    M. Stickel: ‘A Unification Algorithm for Assoc. Commutative Functions’, JACM, vol. 28, no.3, 1981Google Scholar
  116. [ST74]
    G.F. Stewart: ‘An Algebraic Model for String Patterns’, Univ. of Toronto, CSRG-39, 1974Google Scholar
  117. [SU65]
    E. Sussenguth: ‘A graph-theoretical algorithm for matching chemical structures’, J. Chem. Doc. 5, 1, 1965CrossRefGoogle Scholar
  118. [SU78]
    P. Szabo, E. Unvericht: ‘The Unification Problem for Distributive Terms’, Univ. Karlsruhe, 1978Google Scholar
  119. [SZ78]
    P. Szabo: ‘Theory of First Order Unification’ (in German, thesis) Univ. Karlsruhe, 1982Google Scholar
  120. [TA68]
    A. Tarski: ‘Equational Logic and Equational Theories of Algebra’, Schmidt et al (eds), Contributions to Mathematical Logic, North Holland, 1968Google Scholar
  121. [TE81]
    H. Tennant. ‘Natural Language Processing’, Petrocelli Books, 1981Google Scholar
  122. [TY75]
    W. Taylor: ‘Equational Logic’, Colloquia Mathematica Societatis Janos Bolya, 1975Google Scholar
  123. [UL76]
    J.R. Ullman: ‘An Algorithm for Subgraph Isomorphism’, JACM, vol. 23, no.1, 1976Google Scholar
  124. [UM64]
    S.H. Unger: ‘CIT — Heuristic Program for Testing Pairs of directed Line Graphs for Isomorphism’, CACM, vol.7, no.1, 1964Google Scholar
  125. [VA75]
    J. van Vaalen: ‘An Extension of Unification to Substitutions with an Application to ATP’, Proc. of Fourth IJCAI, Tbilisi, USSR, 1975Google Scholar
  126. [VO78]
    E. Vogel: ‘Unifikation von Morphismen’, Diplomarbeit, Univ. Karlsruhe, 1978Google Scholar
  127. [VZ75]
    M. Venturini-Zilli: ‘Complexity of the Unification Algorithm for First Order Expression’, Calcolo XII, Easc IV, 1975Google Scholar
  128. [WA77]
    D.H.D. Warren: ‘Implementing PROLOG’, vol. 1 and vol. 2, D.A.I. Research Rep., no. 39, Univ. of Edinburgh, 1977Google Scholar
  129. [WA84]
    Ch. Walther: ‘Unification in Many Sorted Theories’, Univ. Karlsruhe, 1984Google Scholar
  130. [WC76]
    K. Wong, K. Chandra: ‘Bounds for the String Editing Problem’, JACM, vol. 23, no.1, 1976Google Scholar
  131. [WE73]
    P. Weiner: ‘Linear Pattern Matching Algorithms’, IEEE Symp. on SW. and Automata Theory, 14, 19773Google Scholar
  132. [WH98]
    N. Whitehead: ‘Treatise on Universal Algebra’, 1898Google Scholar
  133. [WI76]
    van Wijngaarden (et all): ‘Revised Rep. on the Algorithmic Language ALGOL68’, Springer-Verlag, Berlin, Heidelberg, N.Y., 1976Google Scholar
  134. [WN75]
    Winston: ‘The Psychology of Computer Vision’, McGraw Hill, 1975Google Scholar
  135. [WN76]
    G. Winterstein: ‘Unification in Second Order Logic’, Bericht 3, Univ. Kaiserslautern, 1976Google Scholar
  136. [WR67]
    L. Wos, G.A. Robinson, D. Carson, L. Shalla: ‘The Concept of Demodulation in Theorem Proving’, JACM, vol. 14, no.4, 1967Google Scholar
  137. [WR73]
    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, 1973Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Jörg H. Siekmann
    • 1
  1. 1.FB InformatikUniversität KaiserslauternKaiserslautern

Personalised recommendations