{"entities":{"Q2218426":{"pageid":2229169,"ns":120,"title":"Item:Q2218426","lastrevid":71584314,"modified":"2026-04-13T23:13:16Z","type":"item","id":"Q2218426","labels":{"en":{"language":"en","value":"A mechanized refinement proof of the Chase-Lev deque using a proof system"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7296761"}},"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":"Q2218426$BF95477A-B32B-41A1-B732-91115D1B2115","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1352fc383c77fec4f60a3f7d716e8920f6842b6b","datavalue":{"value":{"text":"A mechanized refinement proof of the Chase-Lev deque using a proof system","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2218426$8F6FE3F5-F3E9-4EC9-B66D-A1C5DACCE5C2","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d3a9567b8c3bc6721243e2798f9f88f9cd21ebbd","datavalue":{"value":"1458.68276","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2218426$5EAFF550-074C-40B8-AC0A-58C9F7EC6664","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ade2e4ca7131e43c6fa40bcd6a114283377750fc","datavalue":{"value":{"entity-type":"item","numeric-id":2164257,"id":"Q2164257"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2218426$66B8B133-3FFA-424A-9BA9-41610DF102B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"efc258155bc6debe998a6723e056c58cf0faa3b9","datavalue":{"value":{"entity-type":"item","numeric-id":2050103,"id":"Q2050103"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2218426$C9082D1E-9EC6-4284-BC60-6AFB5D483A39","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b79ece58f33b59758a066cb6b9ee149bab3a2c9a","datavalue":{"value":{"entity-type":"item","numeric-id":167642,"id":"Q167642"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2218426$052AE3DE-CFB5-4044-A5FE-B004912CE2B0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5d36ad50495f691273749b6dd2a33c6166368073","datavalue":{"value":{"time":"+2021-01-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2218426$5F6E1D3F-0BC2-4795-853B-7C58E39ECDBC","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"1de3565cfd3393000dd87ca545f95ff84d4c1446","datavalue":{"value":"68W10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2218426$AAC6332B-E7E3-4BA9-A9A3-E081AC69C6F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"14cf74de25853c940589b125137b792dfb2d092b","datavalue":{"value":"68P05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2218426$74A746D7-CB8B-4F66-A743-EEDC3C6D2A26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2218426$DE567A8B-6055-424D-9876-750D446203BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2218426$6E151AF4-EECB-4FA5-A579-457CB6FFA546","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2a78c2e9b0545db97bf30ed1528713c1d973ce07","datavalue":{"value":"7296761","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2218426$FB5D8B22-E244-43BD-A89A-BD8EAC46CDBF","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ea8715b160ad7ce5ee9ef5929b1c64848c500f4","datavalue":{"value":"Chase-Lev deque","type":"string"},"datatype":"string"},"type":"statement","id":"Q2218426$6793CC71-56BE-4C04-8F89-49A177E62B66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"41fc0e1aa1a2e0af898c65e8fb3452317391be07","datavalue":{"value":"Owicki-Gries method","type":"string"},"datatype":"string"},"type":"statement","id":"Q2218426$F18C2412-1C19-4249-AF73-FBA8E78086BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfc1c912dbc1f534d35dfe4c7b828346e80b5fd8","datavalue":{"value":"reduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2218426$4A312FEC-F659-4AD3-BB85-8DE08A8AE092","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e404e0d47002bfb1532cb42cfe324606a2151619","datavalue":{"value":"abstraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2218426$F7AB3B21-0169-4345-A2D5-D396A11394B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ab20a0363e682206851b94b3be1e96bb56399f58","datavalue":{"value":"refinement","type":"string"},"datatype":"string"},"type":"statement","id":"Q2218426$6447E1B1-BF7B-4CB7-95ED-2BAD2AB780EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"06ee1e819076ef64349ed3cd4ccae4a1cbb26c48","datavalue":{"value":"linearizability","type":"string"},"datatype":"string"},"type":"statement","id":"Q2218426$5CBA6811-A813-493F-A702-215AAA608F51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"429b1bb2880597c2344753195d527743940fb5f0","datavalue":{"value":"static verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2218426$6E0AA664-5071-4F0D-95E0-217CF571F20F","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":"Q2218426$84039E0D-440D-46C2-8576-57B41446B694","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"db5447954fc92d44331bba0bd4da114a10521d05","datavalue":{"value":"https://doi.org/10.1007/s00607-018-0635-4","type":"string"},"datatype":"url"},"type":"statement","id":"Q2218426$8E3D3637-FF6C-41D6-A428-D0A9CF5E7894","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"2afbd07dd70190db9f69680f937cfd2e008e8f4a","datavalue":{"value":"W4242282547","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2218426$78374C1D-7ACC-4913-92E9-C344EB52D46D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1ef109aa111718a526718a405487041a4cfc7c7a","datavalue":{"value":{"entity-type":"item","numeric-id":5946213,"id":"Q5946213"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2218426$998CBA89-AA44-45C1-8FC8-941199C00AC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0c515b27ce0877f863df3853a58317bf54103af4","datavalue":{"value":{"entity-type":"item","numeric-id":2819810,"id":"Q2819810"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2218426$4C1DA96E-27DE-42C8-8AC9-72916F629251","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d7a437b3debfc6e39e14adc5ae5b77545ffa37fb","datavalue":{"value":{"entity-type":"item","numeric-id":5261501,"id":"Q5261501"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2218426$B524A185-B223-48D9-B52C-0C0B0EA833AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05656618a7fbd87833428b51ffbb73b7b47e20fc","datavalue":{"value":{"entity-type":"item","numeric-id":4077431,"id":"Q4077431"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2218426$F7EBF2FB-F0B8-4C7A-9BF8-A8FE8DC16D36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"796364eeefb9789a01eab3a144d0337d6c23ee01","datavalue":{"value":{"entity-type":"item","numeric-id":1219675,"id":"Q1219675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2218426$A74F64B7-EBCE-43D1-B2D6-2AEF28821350","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"509f105d86f7909ae4a8a9668b4cbb8d33881027","datavalue":{"value":"Q129608023","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2218426$36C16C70-A905-4E42-A757-69DDFFB74411","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b830eb8adc845d1e9e16dc106b1449b6777c2859","datavalue":{"value":"10.1007/S00607-018-0635-4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2218426$8563EA61-88CC-4F2A-B825-85AD28842DC1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0fe37730f014137665e3503d6006520dbea031ac","datavalue":{"value":{"entity-type":"item","numeric-id":2946743,"id":"Q2946743"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3ee42fbe5a3f09ecfe392de689d1e03b5e41e4d2","datavalue":{"value":{"amount":"+0.7764487266540527","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":"Q2218426$11AE8F41-2B51-4585-92D5-EB4AFF88DA96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ef896335a236046a69e40d814b99d8c75b41a062","datavalue":{"value":{"entity-type":"item","numeric-id":2842111,"id":"Q2842111"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b70400cbc1d18d39336488dfec998051de321551","datavalue":{"value":{"amount":"+0.7601230144500732","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":"Q2218426$815A85C2-F56F-43A9-B188-82F9E6EDF187","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0fc0d1144d70c0b6cd329c4c6118b815cc0993b6","datavalue":{"value":{"entity-type":"item","numeric-id":5246726,"id":"Q5246726"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"19b28813039993135d54fca32eb8fa1545c79f84","datavalue":{"value":{"amount":"+0.7598681449890137","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":"Q2218426$CF336FE4-2E60-41CA-9F22-889C63C5FAEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cbbd115948536399f88bcc955f5a031b25d01e93","datavalue":{"value":{"entity-type":"item","numeric-id":2164258,"id":"Q2164258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e548b6169016bd432b58053088264b5787ba052d","datavalue":{"value":{"amount":"+0.7507216930389404","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":"Q2218426$0285FA3D-32BB-4E47-94D4-8488B2040C64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f759f321f17edf59634b6b68731cb858a7d50353","datavalue":{"value":{"entity-type":"item","numeric-id":3608884,"id":"Q3608884"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6f985a098996963995ba2615811a034525e9c063","datavalue":{"value":{"amount":"+0.7391753196716309","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":"Q2218426$D8E5EC94-4B62-4696-91FE-C8F4EE2BB3BC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A mechanized refinement proof of the Chase-Lev deque using a proof system","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_mechanized_refinement_proof_of_the_Chase-Lev_deque_using_a_proof_system"}}}}}