{"entities":{"Q1109019":{"pageid":1119768,"ns":120,"title":"Item:Q1109019","lastrevid":66687300,"modified":"2026-04-12T11:58:54Z","type":"item","id":"Q1109019","labels":{"en":{"language":"en","value":"A unification algorithm for second-order monadic terms"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4068828"}},"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":"Q1109019$7B3A41A2-9EC3-4669-B3AE-034198C54E1E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"88eca6863389bb2003f5a806abebdeb048204d37","datavalue":{"value":{"text":"A unification algorithm for second-order monadic terms","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1109019$2806458F-D06B-40C9-8B08-1FF2720BD7DD","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a0a99e444aa1e1a6e4335c00d145b46c811b0ec0","datavalue":{"value":"0655.03004","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1109019$FAC72044-6BDA-403E-AF68-FAB72462102E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a4b8bd78142e82b3d1a4ffc73093f88e38a98722","datavalue":{"value":"10.1016/0168-0072(88)90015-2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1109019$AD8A3139-A915-4240-B989-AC7962564D96","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"596956d13d65318c3063740527340bc624646ab6","datavalue":{"value":{"entity-type":"item","numeric-id":174773,"id":"Q174773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1109019$F0AE02FB-0906-4782-AB58-219EACF129DC","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1109019$B8DBE111-D5CD-4153-907B-C1141C74297B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"31a1937240ca4a323604b4728c31d242b5596d7c","datavalue":{"value":{"time":"+1988-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":"Q1109019$DBABE275-7D5F-47ED-ABDF-79607EE34639","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"7ad17048aa0a683364597508fb814844f11f635e","datavalue":{"value":"The paper presents an algorithm for simultaneous unification of finite sets E of pairs of second-order terms which contain no function constants with arity greater than or equal to two. In fact the algorithm is not only a decision procedure. It generates a set \\({\\mathcal U}(E)\\) of substitution schemata such that: \\({\\mathcal U}(E)=\\emptyset\\) iff E is not unifiable and for all substitutions \\(\\sigma\\), \\(\\sigma\\) unifies E iff \\(\\sigma\\) is an instance of some member of \\({\\mathcal U}(E)\\). It has strong similarities with Huet's algorithm for second order monadic terms except that it works with ``parameterized terms'' and ``parameterized substitutions''. In this way it terminates on all inputs and \\({\\mathcal U}(E)\\) is finite in all cases. However for some unifiers only an ``initial segment'' of the unifier is characterized explicitly in \\({\\mathcal U}(E)\\). A preliminary version of the algorithm has appeared in the author's Ph. D. thesis and it has proven to be very useful for investigating some proof complexity problems. The paper is self- contained. Not only are the procedures provided but also the necessary proofs and definitions.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1109019$89DF45D6-417D-4B3C-9CCE-B11EAE034059","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1109019$F519B24B-D2DF-4515-990B-DBC9CDF102CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed4ac44229a63771ae4ded31038fe93f434bffb7","datavalue":{"value":"03C05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1109019$CB2E31C1-3123-4D27-A938-96B9C11578A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1109019$A6CD57E7-CB04-472E-9001-987FFEB22449","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"cb2d8541d69fcd0514a9e56657a261e70035319c","datavalue":{"value":"4068828","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1109019$5E003A4A-296A-4B36-BFF0-A015CC86A496","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c3922eb0b8235fb2b824bcb3eaa0c8d395dbd512","datavalue":{"value":"unification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1109019$D51F7632-B9A8-4E2E-9C41-F4A7D1ECD3CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5fba7c6bba591d632585d3bbd3c5ce6894e9b0bd","datavalue":{"value":"second-order terms","type":"string"},"datatype":"string"},"type":"statement","id":"Q1109019$612C1EC4-7F21-447C-8B9F-61C9F919E4F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"48ddf43eca498c7e7087cd696beb82ea63925320","datavalue":{"value":"algorithm","type":"string"},"datatype":"string"},"type":"statement","id":"Q1109019$1831AC11-DEAC-430B-9D5C-68A485E47C3C","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"6536f759dee9ce142c834adc5cc137400d919eb8","datavalue":{"value":{"entity-type":"item","numeric-id":1037240,"id":"Q1037240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1109019$AF8F33F6-33CD-4F2C-9D26-1D49D485676A","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":"Q1109019$3F70C284-E9B5-4678-A61F-742FBC0240A3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"498b31ad816e2195496144aed47d537dd80e3a32","datavalue":{"value":"https://doi.org/10.1016/0168-0072(88)90015-2","type":"string"},"datatype":"url"},"type":"statement","id":"Q1109019$9E35953D-CE1C-4523-9DA5-C959AAE85B13","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"aef378bd7c3c817072412645e37839d0dcb1b39f","datavalue":{"value":"W2074213277","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1109019$5F2AB10B-EC9E-4F56-ABC8-CF9E1BCB5F49","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c9f2843640e7eabb53dcf6b38d2e418915c6350","datavalue":{"value":{"entity-type":"item","numeric-id":3343471,"id":"Q3343471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1109019$EE60A090-6F15-4DA7-8EEE-E2778F40B3B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f3b8a8bbc08f166f4f946f3a032d3d7074f3fd6b","datavalue":{"value":{"entity-type":"item","numeric-id":1353977,"id":"Q1353977"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1109019$0316A496-D931-4187-9D50-F3AB2C46EDC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7021c91f6a866e16b579f74b23aa54446a0c8938","datavalue":{"value":{"entity-type":"item","numeric-id":1150586,"id":"Q1150586"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1109019$1BF4061C-325F-41F9-B3F8-FF7CBE244D41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b46bb376c314f83419411954235d6e359ad5cbf4","datavalue":{"value":{"entity-type":"item","numeric-id":5672888,"id":"Q5672888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1109019$5C942FB2-50FF-4EE8-A60A-C13C1EC1100E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4fecc7ce8fe53bf0ab0f560a96ff760721b70f9b","datavalue":{"value":{"entity-type":"item","numeric-id":1230505,"id":"Q1230505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1109019$33C7C01E-98FF-4642-BB6A-6F821EB75580","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a9d0de0ba52048b2594da38e4815945e3a42363a","datavalue":{"value":{"entity-type":"item","numeric-id":1251063,"id":"Q1251063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1109019$1A2622A0-D463-4E16-9C2A-097E6E17DDD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b49267d5a56c68e91aab1169da27d04cb8335482","datavalue":{"value":{"entity-type":"item","numeric-id":3843658,"id":"Q3843658"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1109019$430E19AB-FD0A-4CCF-8DE4-780C6FBCCB79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ad0652c94870cdb1bc050ea1ab6ed0f57c34318","datavalue":{"value":{"entity-type":"item","numeric-id":3843659,"id":"Q3843659"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1109019$A6C402A7-86A0-4656-A38F-DB4D1694E182","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"065ea4604210f6f33929664cd3c1938f56d2a34a","datavalue":{"value":{"entity-type":"item","numeric-id":4179180,"id":"Q4179180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1109019$D066977A-12E4-4010-BED6-A739475BB45B","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":"Q1109019$CE0995BA-B6AF-4C1C-B646-55B6AE0D87B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4413667b942f6f696a49dd6b29a6b1aae331dd9f","datavalue":{"value":{"entity-type":"item","numeric-id":3751042,"id":"Q3751042"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1109019$FE2F9B74-98E1-4584-9A19-B726B11E4DA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b9378587a1115a0250a2395ebd434016b1bcd6dd","datavalue":{"value":{"entity-type":"item","numeric-id":4124795,"id":"Q4124795"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1109019$7E80AABE-B890-460E-BC93-B155FB135C73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ab8d7dcc337f0f7083d889ef5fbd195dbcbfcdc2","datavalue":{"value":{"entity-type":"item","numeric-id":4720797,"id":"Q4720797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1109019$7A5F49A1-427B-496A-BA71-5D71E1155E57","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":"Q1109019$D8A065E4-945A-49F3-9748-DAF38D8BBFC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65a7d163034968b8b573af486389b73d9c031e2e","datavalue":{"value":{"entity-type":"item","numeric-id":3707399,"id":"Q3707399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1109019$0C50D775-ADDA-493B-9130-99602971249A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"44f30d6e38a2272ec4079deb3db072ee1d1c745b","datavalue":{"value":{"entity-type":"item","numeric-id":4146715,"id":"Q4146715"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1109019$323E66C6-A59D-448F-974D-0ACD760778E1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a564069e267b514ca61fa4871b9e75c56cd967ed","datavalue":{"value":{"entity-type":"item","numeric-id":3631904,"id":"Q3631904"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5e80a3739d63b5377667362e0f85bba4e61c1f8c","datavalue":{"value":{"amount":"+0.9405698","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1109019$D2B9919B-6BAC-48DF-B877-4569B9631C32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad38cbe209617bc25cf7a748227fcaef91ef0d2e","datavalue":{"value":{"entity-type":"item","numeric-id":5901562,"id":"Q5901562"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d1381facd3baa7198b790a0ef5218f4b77342f52","datavalue":{"value":{"amount":"+0.92033094","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1109019$A11A2AB1-6629-42DD-A691-F76548503CC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"861b4feaeab1f1774c19e2c5a0a646ea159cf413","datavalue":{"value":{"entity-type":"item","numeric-id":1083189,"id":"Q1083189"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"357a65686405c18e06bba471174beaf464067931","datavalue":{"value":{"amount":"+0.8909689","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1109019$0ABD09F4-9956-4988-B28F-228CDB33D1E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bf31fd13c3ece96532629b6df6054d5c03f3958a","datavalue":{"value":{"entity-type":"item","numeric-id":4808756,"id":"Q4808756"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"08fd7d0b1b815999b31ee0ae25742bdc49510e9c","datavalue":{"value":{"amount":"+0.8732003","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1109019$88F4E1ED-99A2-4EBD-A0BA-C45A9AF93DBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"143c30a47b59a0b6c67ef0aebd1260ade2fc8bdb","datavalue":{"value":{"entity-type":"item","numeric-id":3575301,"id":"Q3575301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ef6947bda39a2a9d4f8f36bfa8c46632a896d0d1","datavalue":{"value":{"amount":"+0.8694254","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1109019$5C0B2BCA-4CFA-4261-85DC-024F4C1B2422","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"91022e9178a1fe8f54724eef76647b85356a3d2a","datavalue":{"value":{"entity-type":"item","numeric-id":1295371,"id":"Q1295371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c52a715078af7f29de9c9ec32f3e260b56eb38f4","datavalue":{"value":{"amount":"+0.8673246","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1109019$1618218D-AC77-4353-B814-D335E8F93023","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d39267d2bdc0847c9ec689f4c044e1b228b4fca5","datavalue":{"value":{"entity-type":"item","numeric-id":3586053,"id":"Q3586053"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"14b9d641c05871ad989216515c4bf9138ab0d567","datavalue":{"value":{"amount":"+0.86589193","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1109019$9BD65400-963E-49E0-81C5-100ED077DB3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3523bbfd69c25f4378970fae3afc5c0010522466","datavalue":{"value":{"entity-type":"item","numeric-id":3585001,"id":"Q3585001"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3f771cc989815d564a2df996f4562215acaa9b02","datavalue":{"value":{"amount":"+0.865481","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1109019$AACC2407-3CCC-4E5B-8C3A-0869E2E9F8F2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A unification algorithm for second-order monadic terms","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_unification_algorithm_for_second-order_monadic_terms"}}}}}