{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:23Z","timestamp":1749125183494,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540191292"},{"type":"electronic","value":"9783540391265"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1988]]},"DOI":"10.1007\/3-540-19129-1_4","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T20:03:50Z","timestamp":1330200230000},"page":"67-113","source":"Crossref","is-referenced-by-count":14,"title":["Unification revisited"],"prefix":"10.1007","author":[{"given":"J -L.","family":"Lassez","sequence":"first","affiliation":[]},{"given":"M. J.","family":"Maher","sequence":"additional","affiliation":[]},{"given":"K.","family":"Marriott","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"4_CR1","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C.L. Chang","year":"1973","unstructured":"Chang, C.L. and Lee, R. [1973] Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973."},{"key":"4_CR2","unstructured":"Colmerauer, A. [1984] Equations and Inequations on Finite and Infinite Trees, FGCS'84 Proceedings, Nov. 1984, 85\u201399."},{"key":"4_CR3","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/S0747-7171(85)80027-4","volume":"1","author":"E. Eder","year":"1985","unstructured":"Eder, E. [1985] Properties of Substitutions and Unifications, Journal of Symbolic Computation, 1985, 1, 31\u201346.","journal-title":"Journal of Symbolic Computation"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Herbrand, J. [1930] Recherches sur la theorie de la demonstration (These), Universite de Paris. (In: Ecrits logiques de Jacques Herbrand, Paris, PUF, 1968).","DOI":"10.3917\/puf.herbr.1968.01.0031"},{"key":"4_CR5","unstructured":"Huet, G. [1976] Resolution d'Equations Dans Des Langages D'Ordre, 1, 2,...,\u03c9 (These d'Etat), Universite de Paris VII, Dec. 1976."},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Huet, G. and Oppen, D.C. [1980] Equations and Rewrite Rules: A Survey, Formal Languages: Perspectives and Open Problems, (R. Book Ed.), Academic Press, 1980.","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Jaffar, J. and Lassez, J-L. [1987] Constraint Logic Programming, Proc. POPL'87, January 1987, 111\u2013119.","DOI":"10.1145\/41625.41635"},{"key":"4_CR8","unstructured":"Kirchner, C. and Lescanne, P. [1987] Solving Disequations, Proc. Logic in Computer Science Conf., to appear."},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Kunen, K. [1987a] Negation in Logic Programming, Journal of Logic Programming, to appear.","DOI":"10.1016\/0743-1066(87)90007-0"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Kunen, K. [1987b] Answer Sets and Negation as Failure, Proc. ICLP 4, MIT Press, May 1987, 219\u2013228.","DOI":"10.1016\/0743-1066(87)90007-0"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Lassez, J-L. and Marriott, K.G. [1986] Explicit Representation of Terms Defined by Counter Examples, Proc. FST & TCS Conference, LNCS 241, December 1986. Full version to appear in Journal of Automated Reasoning.","DOI":"10.1007\/3-540-17179-7_6"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Lloyd, J.W. [1984] Foundations of Logic Programming, Springer-Verlag, 1984.","DOI":"10.1007\/978-3-642-96826-6"},{"key":"4_CR13","unstructured":"Maher, M.J. [1987] Logic Semantics for a Class of Committed-choice Programs, Proc. ICLP 4, MIT Press, May 1987, 858\u2013876."},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Makowsky, J. [1984] Model Theoretic Issues in Theoretical Computer Science Part 1: Relational Databases and Abstract Data Types, Logic Colloquium 82, (G. Lolli, G. Longo & A. Marcja Eds.), Elsevier, 1984.","DOI":"10.1016\/S0049-237X(08)71821-4"},{"issue":"2","key":"4_CR15","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"Martelli, A. and Montanari, U. [1982] An Efficient Unification Algorithm, TOPLAS, Vol. 4, No. 2, April 1982, 258\u2013282.","journal-title":"TOPLAS"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Manna, Z. and Waldinger, R. [1980] Problematic Features of Programming Languages: a Situational-calculus Approach, Report No. STAN-CS-80-779, Stanford University, 1980.","DOI":"10.1007\/BF00264494"},{"key":"4_CR17","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/0167-6423(81)90004-6","volume":"1","author":"Z. Manna","year":"1981","unstructured":"Manna, Z. and Waldinger, R. [1981] Deductive Synthesis of the Unification Algorithm, Science of Computer Programming, Vol 1, 5\u201348, 1981.","journal-title":"Science of Computer Programming"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Naish, L. [1986] Negation & Quantifiers in NU-Prolog, Proc. 3rd Conf. on Logic Programming, LNCS 225, 624\u2013634, July 1986.","DOI":"10.1007\/3-540-16492-8_111"},{"issue":"2","key":"4_CR19","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1016\/0022-0000(78)90043-0","volume":"16","author":"M. Paterson","year":"1978","unstructured":"Paterson, M. and Wegman, M. [1978] Linear Unification, Journal of Computer and System Sciences, Vol 16, No 2, 1978, 158\u2013167.","journal-title":"Journal of Computer and System Sciences"},{"key":"4_CR20","unstructured":"Plotkin, G. [1970] A Note on Inductive Generalization, Machine Intelligence 5, (B. Meltzer & D. Michie Eds.), 1970 153\u2013163."},{"key":"4_CR21","unstructured":"Plotkin, G. [1971] A Further Note on Inductive Generalization, Machine Intellgence 6, (B. Meltzer & D. Michie Eds.), 1971, 101\u2013124."},{"key":"4_CR22","unstructured":"Reynolds, J. [1970] Transformational Systems and the Algebraic Structure of Atomic Formulas, Machine Intelligence 5, (B. Meltzer & D. Michie Eds.), 1970, 135\u2013152."},{"issue":"1","key":"4_CR23","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A. [1965] A Machine-Oriented Logic Based on the Resolution Principle, JACM, Vol. 12, No. 1, Jan. 1965, 23\u201341.","journal-title":"JACM"},{"key":"4_CR24","volume-title":"Logic: Form and Function \u2014 The Mechanization of Deductive Reasoning","author":"J.A. Robinson","year":"1979","unstructured":"Robinson, J.A. [1979] Logic: Form and Function \u2014 The Mechanization of Deductive Reasoning, North-Holland, New York, 1979."},{"key":"4_CR25","unstructured":"Sato, T. [1986] Declarative Logic Programming, Research Memo, Electrotechnical Laboratory, 1986."},{"key":"4_CR26","unstructured":"Sterling, L. and Shapiro, E.Y. [1986] The Art of PROLOG, MIT Press, 1986."},{"key":"4_CR27","unstructured":"Vere, S.A. [1975] Induction of Concepts in the Predicate Calculus, IJCAI-75, 1975, 281\u2013287."},{"key":"4_CR28","unstructured":"Vere, S.A. [1977] Induction of Relational Productions in the Presence of Background Information, IJCAI-77, 1977, 349\u2013355."}],"container-title":["Lecture Notes in Computer Science","Foundations of Logic and Functional Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-19129-1_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T20:43:18Z","timestamp":1742589798000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-19129-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988]]},"ISBN":["9783540191292","9783540391265"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-19129-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1988]]}}}