{"entities":{"Q2147186":{"pageid":2157929,"ns":120,"title":"Item:Q2147186","lastrevid":73434951,"modified":"2026-04-14T15:58:14Z","type":"item","id":"Q2147186","labels":{"en":{"language":"en","value":"A verified decision procedure for orders in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7546599"}},"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":"Q2147186$536AE381-6066-41D6-AF8E-38E8656B13A8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f8c520b1aff583258d2b50d1aec7d5b21fa4557d","datavalue":{"value":{"text":"A verified decision procedure for orders in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2147186$EE0FD4BA-EBFE-4FC3-B22E-871A001DF661","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f7acdabe599c7fe4fed6a0863c74916af6bfd7f4","datavalue":{"value":"1497.68549","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2147186$172B9A93-E6EC-4385-AF9C-6BB1485FA170","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0a999734516af67fbe851e0f6618a63a0f8068d8","datavalue":{"value":"10.1007/978-3-030-88885-5_9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2147186$23FDAC45-70EF-45FE-A497-1F9E985D6BE1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3df9e99a8d3ca3fe964f70b9fb2cabb2b706a85d","datavalue":{"value":{"entity-type":"item","numeric-id":2147185,"id":"Q2147185"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147186$A65AFC29-C4A8-47A4-A09D-ADA94C27F057","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bd39997decddd4925a8ef09cbbffc4f41d2b1f00","datavalue":{"value":{"entity-type":"item","numeric-id":670700,"id":"Q670700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147186$0C57D4A0-E868-432A-8850-E1BB5FFB7514","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ffa612dd361e50848b97ee1c8010430ebd9d5009","datavalue":{"value":{"time":"+2022-06-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2147186$F24F27A0-8310-4EB6-A555-F1FA5CD8D373","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7995f57cb4cb03f2a7d81a16ee719381747b55f5","datavalue":{"value":"https://arxiv.org/abs/2104.13117","type":"string"},"datatype":"url"},"type":"statement","id":"Q2147186$1E6990C4-9FF1-4B36-9F29-E794596344D4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2147186$E6E29906-8FB5-4078-921C-37C4AE416BF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2147186$9F7C5137-ABDD-4525-8622-B83414A9F29F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2147186$D7E8B471-91F7-4463-A3D5-71B9C20237A3","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"07daa7ed225926090c1b02d66b0289ac040cd220","datavalue":{"value":"7546599","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2147186$EDDE4D4F-2A43-411F-B9D9-6F12BF8529DB","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147186$B074B522-52CB-49BC-B710-49A21C2FE647","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e338912f65cbd77347bbd512933e55736ef58bd1","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147186$FD009314-BA27-4CDB-ACE0-3B55878A136C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ecf052c5bb7181e8330aefdad108e67bd3e0ce36","datavalue":{"value":{"entity-type":"item","numeric-id":5975195,"id":"Q5975195"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147186$98BEE5D6-52B0-4042-BAFD-70C8C0C059D0","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":"Q2147186$32D97940-CDE5-4853-80AA-0676DD55DB17","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"332554005e67980ef155d8a830ea2bbfff48e0c6","datavalue":{"value":"W3208388410","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2147186$CFB3C971-8CE2-48D2-9CB6-FE2782E961CB","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"12e4cb046e7e6d1eac10022f3d396c57882b72a6","datavalue":{"value":{"entity-type":"item","numeric-id":2754030,"id":"Q2754030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147186$0B8D8A6C-4CD6-4165-A032-B118855ED3FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da0d795517e293a55fbffeee6d84c637293c8bf8","datavalue":{"value":{"entity-type":"item","numeric-id":5327339,"id":"Q5327339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147186$33864BCD-B3A7-477D-A3A2-B0B73A44DCEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"70415211cfe84908ddcdabfc0c0a97bbbc2328dc","datavalue":{"value":{"entity-type":"item","numeric-id":5824365,"id":"Q5824365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147186$500796E7-8E6E-4BCA-82C7-5D76ABDD90DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b54f7383e1361db9b7d8d635e3974eec1f15734d","datavalue":{"value":{"entity-type":"item","numeric-id":5536269,"id":"Q5536269"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147186$BAC2C3BC-E593-43D0-A15C-DA0462BE50F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"75cb010ae1c1f82f142d7f1427cb01809e5c6acc","datavalue":{"value":{"entity-type":"item","numeric-id":701722,"id":"Q701722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147186$AFB283C7-777A-4CDC-B0D0-95C4999B1070","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d18a95fd2abb64fb3873cebae9515dbda415b84","datavalue":{"value":{"entity-type":"item","numeric-id":3541684,"id":"Q3541684"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147186$246F1155-E13B-4FC5-8B85-6FE3598F3A77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2147186$EFDCA4F9-35CF-4978-ACC0-E59CFC1F7569","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4826a9ebcee41c22e639fb6a714a4c993eaa4703","datavalue":{"value":{"entity-type":"item","numeric-id":707743,"id":"Q707743"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eff9d71634e178ef3df685dece69a8613b124ac9","datavalue":{"value":{"amount":"+0.83143150806427","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":"Q2147186$74C81078-7082-4AA6-889F-A5252AA69BBD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b19f108f54644f0ec26605a1f87cb8a667d4c8a5","datavalue":{"value":{"entity-type":"item","numeric-id":3541684,"id":"Q3541684"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b0a48500f7134dae63d37591cd1c12a8488bdd68","datavalue":{"value":{"amount":"+0.8194841742515564","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":"Q2147186$D50E1B2F-5EED-438F-B243-32431F10A4A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e276227318e6725fab8632c8a3a0db57cfb2367a","datavalue":{"value":{"entity-type":"item","numeric-id":5505503,"id":"Q5505503"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7abc2e457b30eca80ba9e1a9bcc6f063912b4efc","datavalue":{"value":{"amount":"+0.7906457185745239","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":"Q2147186$04C6F52C-4AB2-40D3-A82B-85F0A4792882","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9c83d06f502aa0ec7275e55aad7398af4dbb019a","datavalue":{"value":{"entity-type":"item","numeric-id":3559760,"id":"Q3559760"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2eb95e5ccb6fd58d1b3078371303aaadd94bdf09","datavalue":{"value":{"amount":"+0.779911458492279","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":"Q2147186$27873B2E-3C06-458E-BFAD-6778314F1D97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9c87fc5ea61279fa36596c30cb797ea88bc4ea2b","datavalue":{"value":{"entity-type":"item","numeric-id":5234694,"id":"Q5234694"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2e5e71f71b4055b21d7106e92a9510dc6f77172a","datavalue":{"value":{"amount":"+0.7702391743659973","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":"Q2147186$39F46342-FED0-4A11-9394-E4DB2C73FB7B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A verified decision procedure for orders in Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_verified_decision_procedure_for_orders_in_Isabelle/HOL"}}}}}