{"entities":{"Q1260765":{"pageid":1271515,"ns":120,"title":"Item:Q1260765","lastrevid":68320869,"modified":"2026-04-12T22:54:55Z","type":"item","id":"Q1260765","labels":{"en":{"language":"en","value":"Finite acyclic theories are unitary"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 370654"}},"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":"Q1260765$F4B829CE-F0AD-4744-AA26-BB44B2203DEB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"88f86b8a55ecf1186545ada21cc1cb5577f2ac38","datavalue":{"value":{"text":"Finite acyclic theories are unitary","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1260765$AB1FF298-1AEB-4CC6-866D-04B721153390","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6012284ffda6adc5da250adde2b41b519d80413e","datavalue":{"value":"0777.68070","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1260765$A152DE00-7C64-4EB0-9350-D31290259C73","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c2875d8c3bf5a90838b3f77794d93fe24e6c0fb1","datavalue":{"value":{"entity-type":"item","numeric-id":685422,"id":"Q685422"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1260765$3F44E6D5-756A-40F6-A047-DE8600E76EE7","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":"Q1260765$CB2293C8-DBE2-4139-BBD2-AF740E096146","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"db72996963a9193f3c38ca9de20c1dcbfa0ae1ee","datavalue":{"value":{"time":"+1993-08-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1260765$D95586DE-8225-440C-97DC-21B62A389615","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"83540d12697ea4b673ef202b8078135381b10a33","datavalue":{"value":"The paper deals with unification modulo an equational theory \\(E\\): Given a problem \\(P=\\{u_ i=v_ i\\mid 1\\leq i\\leq n\\}\\), a substitution \\(\\sigma\\) is a solution (a unifier) of \\(P\\) if \\(\\sigma(u_ i)=_ E\\sigma(v_ i)\\) for \\(1\\leq i\\leq n\\). A set \\(M_ E(P)\\) of unifiers is a minimal complete set of unifiers if   (i) any unifier is an \\(E\\)-instance of a substitution \\(M_ E(P)\\) and   (ii) \\(M_ E(P)\\) contains no two substitutions which are \\(E\\)-equal.   Equational theories can be classified according to their minimal complete sets of unifiers. \\(E\\) is called unitary, finitary or infinitary if for every solvable problem \\(P\\) such a set \\(M_ E(P)\\) exists which is a singleton, a finite set or an infinite set, respectively. \\(E\\) is called nullary if for some solvable \\(P\\) no \\(M_ E(P)\\) exists.   Almost nothing is known about which properties of \\(E\\) imply that \\(E\\) is in any of these classes. Clearly, if \\(E=\\emptyset\\) then we have the free unification problem and \\(E\\) is unitary by Robinson's unification algorithm. The paper gives a non-trivial class of equational theories which are unitary: Let \\(E\\) be presented by a finite set \\(E'=\\{s_ i=t_ i| 1\\leq i\\leq m\\}\\). The main result of the paper states that \\(E\\) is unitary if \\(E\\) is finite and \\(E'\\) is acyclic. More precisely, if \\(P=\\{u=v\\}\\) consists of one equation only and there exists an \\(E\\)-unifier of \\(P\\), then \\(M_ E(P)\\) is a singleton. To explain this let \\(top(s)=f\\) if term \\(s\\) has the form \\(s=f(s_ 1,\\dots,s_ n)\\). Now, \\(E\\) is finite, if every \\(E\\)-congruence class is finite. \\(E'\\) is acyclic of   \\((\\alpha)\\) \\(top(s_ i)\\neq top(t_ i)\\) for \\(1\\leq i\\leq m\\),   \\((\\beta)\\) \\(\\{top(s_ i),top(t_ i)\\}\\neq\\{top(s_ j),top(t_ j)\\}\\) for \\(i\\neq j\\) and   \\((\\gamma)\\) for any function symbols \\(f,g\\) there is at most one sequence \\(i_ 1,\\dots,i_ k\\) such that \\(f=top(s_{i_ 1})\\), \\(g=top(t_{i_ k})\\), \\(s_{i_ j}=t_{i_ j}\\) in \\(E'\\) and \\(top(t_{i_ j})=top(s_{i_{j+1}})\\).   An algorithm is given that on input \\(u=v\\) computes a most general \\(E\\)- unifier if its stops and an \\(E\\)-unifier exists. It is conjectured that the algorithm always stops if an \\(E\\)-unifier exists. But, it may not stop if an \\(E\\)-unifier does not exist.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1260765$5304BC51-7440-44E4-B1DE-7463F58F18F5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1260765$4799D216-73DF-49F0-8473-EA3374C08A53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6be78f1bad1f2f19058dbde65eb124c0430a7d27","datavalue":{"value":"68W30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1260765$16B762D6-C644-4294-B271-8A833298DF15","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"810fdcea397670350f260d4a9498d69cb03b186b","datavalue":{"value":"370654","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1260765$E34D479B-B7DA-4C60-A554-E50EDC0255DB","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c3922eb0b8235fb2b824bcb3eaa0c8d395dbd512","datavalue":{"value":"unification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1260765$8DC02E80-B932-479E-BDEC-AB27B8127316","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d649755d7dec7fe8dd2722580b18ccd4bdd91b89","datavalue":{"value":"equational theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1260765$37433980-08E2-41B0-95D4-01C243F89987","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"baa72ef0b4b6f5b7824b86d8a92894fa90a2fa64","datavalue":{"value":"unitary","type":"string"},"datatype":"string"},"type":"statement","id":"Q1260765$5AE69A0B-DA82-466C-A538-57045C44CBC3","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"1024eb68be5ead5b1a13571c300dc7d3374934dc","datavalue":{"value":{"entity-type":"item","numeric-id":174769,"id":"Q174769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1260765$12B01CD3-5AB3-4100-AB06-36DA26286CEC","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":"Q1260765$DC6B34D9-6221-4702-8347-EE0719A6F346","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d5bd240187d92d8419d95ec63cce55af466995ef","datavalue":{"value":"https://doi.org/10.1006/jsco.1993.1017","type":"string"},"datatype":"url"},"type":"statement","id":"Q1260765$9E083CF2-70EA-4185-884E-9FF04203B211","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"cbfd328252e17cf841cced7168ac96cb42815e4f","datavalue":{"value":"W2010973308","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1260765$36234E4D-A4DA-4AB9-A7FF-33E03C105F95","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"94aa35eb4978630b3c9c566fdcc361f02aa59662","datavalue":{"value":"10.1006/JSCO.1993.1017","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1260765$B82F9B77-F3B8-419C-8E0D-C6049388DC9D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"39cefff5977717e3a72fba0ceb63884f6643e966","datavalue":{"value":{"entity-type":"item","numeric-id":3335752,"id":"Q3335752"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d7a80e703a8f8e9de0f0e2ccd9273a76dbc5c444","datavalue":{"value":{"amount":"+0.8218583464622498","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":"Q1260765$1F5AB54A-C29B-475F-B525-FD649043241C","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":"5853e5e5b13088f988a16d5d2ea40786f8b4f9f2","datavalue":{"value":{"amount":"+0.8200841546058655","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":"Q1260765$11491D3F-3A87-4081-9469-D269DD2F7DB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"83e20c3e805256bbc71175fa832cc3b417cb3d20","datavalue":{"value":{"entity-type":"item","numeric-id":3820054,"id":"Q3820054"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4427d2207a3079d58f75c3d1aa99aa532e12a57b","datavalue":{"value":{"amount":"+0.8185807466506958","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":"Q1260765$31BB5985-5557-4476-9673-C8D92C64B399","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f32d6b9d650b40bb4f5a90f869f721fb7569426d","datavalue":{"value":{"entity-type":"item","numeric-id":1825184,"id":"Q1825184"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4524441d6b03d5746cb7ef3354f1c00976ad2183","datavalue":{"value":{"amount":"+0.8183937668800354","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":"Q1260765$78696DA7-6E31-4895-96C1-8D426A3FBB94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5b636f4e8f1fa0aee790a7d6b8190c5680ec0a7d","datavalue":{"value":{"entity-type":"item","numeric-id":3779785,"id":"Q3779785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0898d6e180186de6060e866245782657756581dd","datavalue":{"value":{"amount":"+0.8155561685562134","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":"Q1260765$53114F21-2332-45CF-86CF-2EF5523FB9DC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Finite acyclic theories are unitary","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Finite_acyclic_theories_are_unitary"}}}}}