{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T13:25:56Z","timestamp":1773235556885,"version":"3.50.1"},"reference-count":28,"publisher":"Elsevier","isbn-type":[{"value":"9780934613408","type":"print"}],"license":[{"start":{"date-parts":[[1988,1,1]],"date-time":"1988-01-01T00:00:00Z","timestamp":567993600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1988]]},"DOI":"10.1016\/b978-0-934613-40-8.50019-1","type":"book-chapter","created":{"date-parts":[[2014,7,1]],"date-time":"2014-07-01T16:06:13Z","timestamp":1404230773000},"page":"587-625","source":"Crossref","is-referenced-by-count":132,"title":["Unification Revisited"],"prefix":"10.1016","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":"78","reference":[{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib1","series-title":"Symbolic Logic and Mechanical Theorem Proving","author":"Chang","year":"1973"},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib2","unstructured":"Colmerauer, A. [1984] Equations and Inequations on Finite and Infinite Trees, FGCS'84 Proceedings, 85\u201399"},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib3","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/S0747-7171(85)80027-4","article-title":"Properties of Substitutions and Unifications","volume":"1","author":"Eder","year":"1985","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib4","series-title":"Recherches sur la Theorie de la Demonstration (these)","author":"Herbrand","year":"1930"},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib5","unstructured":"Huet, G. [1976] Resolution d'Equations Dans Des Langages D'Ordre 1, 2, \u2026, \u03c9 (these d'etat), Universite de Paris VII"},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib6","series-title":"Formal Languages: Perspectives and Open Problems","article-title":"Equations and Rewrite Rules: A Survey","author":"Huet","year":"1980"},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib7","doi-asserted-by":"crossref","unstructured":"Jaffar, J. and Lassez, J-L. [1987] Constraint Logic Programming, Proc. POPL'87, 111\u2013119","DOI":"10.1145\/41625.41635"},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib8","unstructured":"Kirchner, C. and Lescanne, P. [1987] Solving Disequations, Proc. Logic in Computer Science Conf."},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib9","doi-asserted-by":"crossref","unstructured":"Kunen, K. [1987a] Negation in Logic Programming, Journal of Logic Programming.","DOI":"10.1016\/0743-1066(87)90007-0"},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib10","series-title":"Answer Sets and Negation as Failure","first-page":"219","author":"Kunen","year":"1987"},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib11","unstructured":"Lassez, J.-L. and Marriott, K. G. [1986] Explicit Representation of Terms Defined by Counter Examples, Proc. FST & TCS Conference, LNCS 241. Full version to appear in Journal of Automated Reasoning."},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib12","series-title":"Foundations of Logic Programming","author":"Lloyd","year":"1984"},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib13","series-title":"Logic Semantics for a Class of Committed-choice Programs","first-page":"858","author":"Maher","year":"1987"},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib14","article-title":"Model Theoretic Issues in Theoretical Computer Science Part 1: Relational Databases and Abstract Data Types","volume":"82","author":"Makowsky","year":"1984"},{"issue":"2","key":"10.1016\/B978-0-934613-40-8.50019-1_bib15","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","article-title":"An Efficient Unification Algorithm","volume":"4","author":"Martelli","year":"1982","journal-title":"TOPLAS"},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib16","series-title":"Problematic Features of Programming Languages: A Situational-Calculus Approach","author":"Manna","year":"1980"},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib17","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1016\/0167-6423(81)90004-6","article-title":"Deductive Synthesis of the Unification Algorithm","volume":"1","author":"Manna","year":"1981","journal-title":"Science of Computer Programming"},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib18","doi-asserted-by":"crossref","unstructured":"Naish, L. [1986] Negation & Quantifiers in NU-Prolog, Proc. 3rd Conf. on Logic Programming, LNCS 225, 624\u2013634","DOI":"10.1007\/3-540-16492-8_111"},{"issue":"2","key":"10.1016\/B978-0-934613-40-8.50019-1_bib19","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1016\/0022-0000(78)90043-0","article-title":"Linear Unification","volume":"16","author":"Paterson","year":"1978","journal-title":"Journal of Computer and System Sciences"},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib20","unstructured":"Plotkin, G. [1970] A Note on Inductive Generalization, Machine Intelligence 5 (B. Meltzer and D. Michie, Eds.), 153\u2013163"},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib21","unstructured":"Plotkin, G. [1971] A Further Note on Inductive Generalization, Machine Intelligence 6 (B. Meltzer and D. Michie, Eds.), 101\u2013124"},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib22","unstructured":"Reynolds, J. [1970] Transformational Systems and the Algebraic Structure of Atomic Formulas, Machine Intelligence 5 (B. Meltzer and D. Michie, Eds.), 135\u2013152"},{"issue":"1","key":"10.1016\/B978-0-934613-40-8.50019-1_bib23","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A Machine-Oriented Logic Based on the Resolution Principle","volume":"12","author":"Robinson","year":"1965","journal-title":"JACM"},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib24","series-title":"Logic: Form and Function\u2014The Mechanization of Deductive Reasoning","author":"Robinson","year":"1979"},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib25","series-title":"Declarative Logic Programming","author":"Sato","year":"1986"},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib26","series-title":"The Art of PROLOG","author":"Sterling","year":"1986"},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib27","unstructured":"Vere, S. A. [1975] Induction of Concepts in the Predicate Calculus, IJCAI-75, 281\u2013287"},{"key":"10.1016\/B978-0-934613-40-8.50019-1_bib28","unstructured":"Vere, S. A. [1977] Induction of Relational Productions in the Presence of Background Information, IJCAI-77, 349\u2013355"}],"container-title":["Foundations of Deductive Databases and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780934613408500191?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780934613408500191?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,8,12]],"date-time":"2019-08-12T08:28:16Z","timestamp":1565598496000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780934613408500191"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988]]},"ISBN":["9780934613408"],"references-count":28,"URL":"https:\/\/doi.org\/10.1016\/b978-0-934613-40-8.50019-1","relation":{},"subject":[],"published":{"date-parts":[[1988]]}}}