{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,22]],"date-time":"2023-10-22T00:01:03Z","timestamp":1697932863126},"reference-count":21,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1985,3,1]],"date-time":"1985-03-01T00:00:00Z","timestamp":478483200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":10365,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Symbolic Computation"],"published-print":{"date-parts":[[1985,3]]},"DOI":"10.1016\/s0747-7171(85)80026-2","type":"journal-article","created":{"date-parts":[[2008,4,9]],"date-time":"2008-04-09T14:00:48Z","timestamp":1207749648000},"page":"7-29","source":"Crossref","is-referenced-by-count":14,"title":["Equational methods in first order predicate calculus"],"prefix":"10.1016","volume":"1","author":[{"given":"Etienne","family":"Paul","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0747-7171(85)80026-2_bib1","doi-asserted-by":"crossref","first-page":"433","DOI":"10.1017\/S0305004100013463","article-title":"On the structure of abstract algebras","volume":"31","author":"Birkhoff","year":"1935","journal-title":"Proc. Cambridge Phil. Soc."},{"key":"10.1016\/S0747-7171(85)80026-2_bib2","first-page":"53","article-title":"Reduction systems and small cancellation theory","author":"Bucken","year":"1979","journal-title":"Proc. Fourth Workshop on Automated Deducti\u00f2n"},{"key":"10.1016\/S0747-7171(85)80026-2_bib3","series-title":"Symbolic Logic and Mechanical Theorem Proving","author":"Chang","year":"1973"},{"key":"10.1016\/S0747-7171(85)80026-2_bib4","series-title":"Formes Canoniques dans les Alg\u00e8bres Bool\u00e9ennes, et Application \u00e0 la Denwnstration Automatique en Logique du Premier Ordre","author":"Fages","year":"1983"},{"key":"10.1016\/S0747-7171(85)80026-2_bib5","article-title":"Rewrite methods for clausal and non-clausal theorem proving","author":"Hsiang","year":"1983","journal-title":"Proc, ICALP 83, Spain"},{"issue":"1","key":"10.1016\/S0747-7171(85)80026-2_bib6","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/0022-0000(81)90002-7","article-title":"A complete proof of correctness of the Knuth-Bendix completion algorithm","volume":"23","author":"Huet","year":"1981","journal-title":"J. Comp. Syst. Sci."},{"key":"10.1016\/S0747-7171(85)80026-2_bib7","series-title":"Formal Languages: Perspectives and Open Problems","article-title":"Equations and rewrite rules: a survey","author":"Huet","year":"1980"},{"key":"10.1016\/S0747-7171(85)80026-2_bib8","article-title":"Canonical form and unification","volume":"87","author":"Hullot","year":"1980"},{"key":"10.1016\/S0747-7171(85)80026-2_bib9","article-title":"Incremental unification in equational theories","author":"Jouannaud","year":"1982","journal-title":"Proc. of the 21st Allerton Conference"},{"key":"10.1016\/S0747-7171(85)80026-2_bib10","article-title":"Confluent and coherent sets of reduction with equations. Application to proofs in data types","author":"Jouannaud","year":"1983","journal-title":"Proc. 8th Colloquium on Trees in Algebra and Programming"},{"key":"10.1016\/S0747-7171(85)80026-2_bib11","series-title":"Computational problems in abstract algebra","first-page":"263","article-title":"Simple word problems in universal algebra","author":"Knuth","year":"1970"},{"key":"10.1016\/S0747-7171(85)80026-2_bib12","series-title":"Canonical Inference","author":"Lankford","year":"1975"},{"key":"10.1016\/S0747-7171(85)80026-2_bib13","author":"Lankford","year":"1978","journal-title":"On Semi-deciding First Order Validity and Invalidity"},{"key":"10.1016\/S0747-7171(85)80026-2_bib14","series-title":"A Completeness Theorem and a Computer Program for Finding Theorems Derivable for Given Axioms","author":"Lee","year":"1967"},{"key":"10.1016\/S0747-7171(85)80026-2_bib15","series-title":"Proc. 9th Colloquium on Trees in Algebra and Programming, Bordeaux (March 1984)","article-title":"Proof by induction in equational theories with relations between constructors","author":"Paul","year":"1984"},{"key":"10.1016\/S0747-7171(85)80026-2_bib16","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","article-title":"Complete sets of reductions for some equational theories","volume":"28","author":"Peterson","year":"1981","journal-title":"J. Assoc. Comp. Mach."},{"key":"10.1016\/S0747-7171(85)80026-2_bib17","series-title":"Machine Intelligence No. 7","first-page":"73","article-title":"Building-in equational theories","author":"Plotkin","year":"1972"},{"key":"10.1016\/S0747-7171(85)80026-2_bib18","series-title":"Etude des Syst\u00e8mes de R\u00e8eriture Conditionnels et Application aux Types Abstraits Alg\u00e8briques","author":"Remy","year":"1982"},{"key":"10.1016\/S0747-7171(85)80026-2_bib19","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":"J. Assoc. Comp. Math."},{"key":"10.1016\/S0747-7171(85)80026-2_bib20","doi-asserted-by":"crossref","first-page":"622","DOI":"10.1145\/321850.321859","article-title":"Automatic theorem proving for theories with simplifiers, commutafivity and associativity","volume":"21","author":"Slagle","year":"1974","journal-title":"J. Assoc. Comp. Mach."},{"key":"10.1016\/S0747-7171(85)80026-2_bib21","doi-asserted-by":"crossref","first-page":"163","DOI":"10.2307\/1969039","article-title":"A remark on functionally free algebras","volume":"47","author":"Tarski","year":"1946","journal-title":"Ann. Math."}],"container-title":["Journal of Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717185800262?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717185800262?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2018,12,30]],"date-time":"2018-12-30T12:29:54Z","timestamp":1546172994000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0747717185800262"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1985,3]]},"references-count":21,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1985,3]]}},"alternative-id":["S0747717185800262"],"URL":"https:\/\/doi.org\/10.1016\/s0747-7171(85)80026-2","relation":{},"ISSN":["0747-7171"],"issn-type":[{"value":"0747-7171","type":"print"}],"subject":[],"published":{"date-parts":[[1985,3]]}}}