{"entities":{"Q1099648":{"pageid":1110400,"ns":120,"title":"Item:Q1099648","lastrevid":69639549,"modified":"2026-04-13T08:23:22Z","type":"item","id":"Q1099648","labels":{"en":{"language":"en","value":"Associative-commutative unification"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4041329"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099648$B6AB5E14-FD2D-41E0-8C83-0A0D16729F24","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fe1194fac3713098828521d92010938a3fcd3591","datavalue":{"value":{"text":"Associative-commutative unification","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1099648$23E27857-B08D-4AF2-8704-38C417BF8C6B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"26956c4cc13f44332855c0d314de01f13db34070","datavalue":{"value":"0638.68103","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1099648$33DB7DBB-9750-4C23-9AE8-45E1A960FA8C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"71d811ae4f80f591077ee96df641d8ee5cbc7863","datavalue":{"value":"10.1016/S0747-7171(87)80004-4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1099648$EFB48A41-12A3-4FD5-88BA-E951AF9AA5A9","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3af5bd70bdf1aab77620ece66f5e40dd3ce66d83","datavalue":{"value":{"entity-type":"item","numeric-id":272012,"id":"Q272012"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099648$5316676F-8C64-49CF-9226-D27D8F0150D3","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ea72303f92787da89554ee5fa15621068821a762","datavalue":{"value":{"entity-type":"item","numeric-id":99061,"id":"Q99061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099648$04ADE261-7830-4018-8271-5C8A2EF4E37A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5ae48c61eed19d1e1e1f33f9255d5b329362d064","datavalue":{"value":{"time":"+1987-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1099648$ECFC6E20-9BD7-40B6-B662-B4CE39E10AC6","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"76aed949e73cb3079f3cb8778dfb881694bc0a05","datavalue":{"value":"Unification in equational theories, that is, solving equations in varieties, is of special relevance to automated deduction. Major results in term rewriting systems, as by \\textit{G. E. Peterson} and \\textit{M. E. Stickel} [J. Assoc. Comput. Mach. 28, 233-264 (1981; Zbl 0479.68092)], depend on unification in presence of associative-commutative functions. \\textit{M. E. Stickel} [ibid. 28, 423-434 (1981; Zbl 0462.68075)] gave an associative-commutative unification algorithm, but its termination in the general case was still questioned.    The first part of this paper is an introduction to unification theory, the second part concerns the solving of homogeneous linear diophantine equations, and the third contains a proof of termination and correctness of the associative-commutative unification algorithm for the general case.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1099648$C2ECB3C3-2BCD-40BC-8320-B7F65A50797B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1099648$D1201622-A6CB-4B3F-B8C5-EBA037D5A46B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4897136ea1c19614fe909b8db60c4ec176d94a78","datavalue":{"value":"08B05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1099648$78E1FFA7-8FF6-4E76-9369-7A0BE38A8980","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f31233b552eca4a4ba62dfc962e070217fef4dcf","datavalue":{"value":"11D04","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1099648$B0C950B2-9E6A-4D58-86E1-E6DD591D609D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"41360e710c04e124515e5c3736f61887c9d1bb91","datavalue":{"value":"4041329","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1099648$88AFCF33-38A8-4D76-98CE-F26C13A5D086","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bf3af4f55700a7d0f245dbbc9c7f2a981f2e6267","datavalue":{"value":"Unification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1099648$EE0EBBF4-B53A-4457-9CA4-5FD23968C9EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8ac708066b077a4cbf2f59c943781969d75d6d03","datavalue":{"value":"equational theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q1099648$8A5E4233-D37F-4B7D-89B6-136575A37315","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a20a062630d1bb5cf9aa5d669cd08fbd3eee7671","datavalue":{"value":"automated deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1099648$B8B9AB4D-E869-4D58-B0ED-210159647BC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e6d6097ecc3ef5eb2cfee6bb975a37f219ed71c1","datavalue":{"value":"associative- commutative functions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1099648$5DFEE16D-AF44-4BA1-892A-100FC7C2535F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9f196e97590eea861b5bb250930f22035acbc5ab","datavalue":{"value":"homogeneous linear diophantine equations","type":"string"},"datatype":"string"},"type":"statement","id":"Q1099648$CFB11B55-0D5E-44B8-A9EB-21A4AEB38C3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4befa4ca20f2beabcfa09e8a92ae13c21cb4934a","datavalue":{"value":"termination","type":"string"},"datatype":"string"},"type":"statement","id":"Q1099648$2417693F-B498-4CB6-944D-8CA0A17C660F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f9ac4ef6ef6c5f8856ee80195276e724e0b6225a","datavalue":{"value":"correctness","type":"string"},"datatype":"string"},"type":"statement","id":"Q1099648$C4AD35BD-745F-43A0-A564-47CAA0183396","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099648$19518D02-381A-4F13-A66E-104E4640D468","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"418759374d5922aabc765b28cbbf0706f691c101","datavalue":{"value":"Q56092434","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1099648$1A828C14-4BB0-49F0-A64B-541D11F64721","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7d6ea43f4539b07f56dc7ca504e383937ea706cf","datavalue":{"value":{"entity-type":"item","numeric-id":3696522,"id":"Q3696522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099648$E2288890-4C9F-450F-B942-6F2F82B5624D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"175c1c6339231426570e05a46d3193da46e70701","datavalue":{"value":{"entity-type":"item","numeric-id":4401926,"id":"Q4401926"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099648$E2591678-29D4-4894-98A4-E85123D89E24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e81d57b58abc3a82b100d072439fecb147f7ea86","datavalue":{"value":{"entity-type":"item","numeric-id":3716320,"id":"Q3716320"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099648$4CD24271-FA51-4803-94C8-152E4CF8DC4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aef54c5db44ce04a09d816f6d39aa5422147f89f","datavalue":{"value":{"entity-type":"item","numeric-id":1820760,"id":"Q1820760"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099648$94F51F91-129D-4FEF-9D9E-CFB99F620F8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eaadc581f1889f5a25b9794a77af10f6ac4d02d8","datavalue":{"value":{"entity-type":"item","numeric-id":3703287,"id":"Q3703287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099648$79801639-B5DF-4140-ADFF-CB37469688EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c5c1ba27129d07dafebc0bafb7063cfc377091f1","datavalue":{"value":{"entity-type":"item","numeric-id":3786019,"id":"Q3786019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099648$026D9185-ADF0-4832-A11C-C09EC185A220","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9ad03955cd9d1b12f908e9f0d19d305e55a944b1","datavalue":{"value":{"entity-type":"item","numeric-id":1246557,"id":"Q1246557"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099648$6A2A2174-D247-4833-8234-73E95F57A28E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6abc42fc8ffc23569c13bf6c75648de9ca35ca32","datavalue":{"value":{"entity-type":"item","numeric-id":3219154,"id":"Q3219154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099648$A4E1EA59-AE51-48EC-98E6-2B1F6A8EAB09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"092348088466a9288a4b352c8d624aae9ff71ffb","datavalue":{"value":{"entity-type":"item","numeric-id":4159542,"id":"Q4159542"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099648$82FA7B2F-C3A2-498F-9CA8-3FC21C641817","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c9465d6417bb77bd19e652eaf6c381784d12e8b","datavalue":{"value":{"entity-type":"item","numeric-id":3936229,"id":"Q3936229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099648$C5567B29-1C51-47B5-8F6D-24FE5DF19D13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8670a1cb5138f59a7607a06c6c33e9eef7f2c9ea","datavalue":{"value":{"entity-type":"item","numeric-id":3938536,"id":"Q3938536"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099648$3C4DA136-6F19-4673-B0A7-8E5CEE8D68A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"10514d04294539f6b18e653ffed15729ce3e519b","datavalue":{"value":{"entity-type":"item","numeric-id":5678447,"id":"Q5678447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099648$4BF7F4D1-80DE-4E0E-9371-06C2B939103C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099648$55D5C124-6E75-48B8-BDC9-F775B88B4338","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1669261077901413d76dc0f7072dfdae93141a3b","datavalue":{"value":{"entity-type":"item","numeric-id":3912070,"id":"Q3912070"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099648$E43795EB-2464-4032-AE98-0C3B547D0581","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e88635d4bbfcc4225b489e70aecd75b03442f6e","datavalue":{"value":{"entity-type":"item","numeric-id":3785922,"id":"Q3785922"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099648$28AF8C94-0E6E-4AFF-A1E2-B9CFCD393309","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e0deeb2cb06267117731d61f48ec1b47953178b6","datavalue":{"value":{"entity-type":"item","numeric-id":3716322,"id":"Q3716322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099648$EFB4BD93-3B52-45A9-9FCA-7E57FE1D49B1","rank":"normal"}],"P1635":[{"mainsnak":{"snaktype":"value","property":"P1635","hash":"f90b769b5fcc763db18f4ee4fd7912ece59e707f","datavalue":{"value":"journals/jsc/Fages87","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1099648$3631EC41-F53F-442C-9CAC-E11E0C147965","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2a15a4817023bf3bc7b69da94d013b6f29b9d70e","datavalue":{"value":{"entity-type":"item","numeric-id":3338216,"id":"Q3338216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7dbb5776fe968b227cfa5e290fc1b3c8097b733d","datavalue":{"value":{"amount":"+0.9087321758270264","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1099648$2AE84CF3-2553-4132-9D96-0754501C2A01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"94a3013126c88788e1f2abca5dc5b703dde202bb","datavalue":{"value":{"entity-type":"item","numeric-id":3805960,"id":"Q3805960"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a55911c726c24de9c275a54e8a6adf76b38367d9","datavalue":{"value":{"amount":"+0.8940209150314331","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1099648$C432378F-2909-40BA-95CC-23FC539AE491","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"17933c17044f6249c98bbea6854df8139e935ea1","datavalue":{"value":{"entity-type":"item","numeric-id":3703287,"id":"Q3703287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a61d56fa730c24bc8784c37d87ba806fef15594a","datavalue":{"value":{"amount":"+0.8868238925933838","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1099648$2E12E238-D7A1-4146-BC48-10398D9B354F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c8074c1975bd09abeafde4674061df377001e043","datavalue":{"value":{"entity-type":"item","numeric-id":1262757,"id":"Q1262757"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0f9120d2a68d37cf18e0738eadd77b88bf436fae","datavalue":{"value":{"amount":"+0.8779479265213013","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1099648$E5F4932F-07BE-4ACD-91E3-0CF8BD253B9F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"215137121412e0b1f51567744bea8f32970209cf","datavalue":{"value":{"entity-type":"item","numeric-id":5096305,"id":"Q5096305"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"177d5ab5291a13d2db9f209861ccb4d2e82d855a","datavalue":{"value":{"amount":"+0.8752358555793762","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1099648$924D6ABD-4C61-45D6-A67F-DAAFD4D42914","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Associative-commutative unification","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Associative-commutative_unification"}}}}}