{"entities":{"Q2945711":{"pageid":2956431,"ns":120,"title":"Item:Q2945711","lastrevid":79790777,"modified":"2026-05-06T14:43:04Z","type":"item","id":"Q2945711","labels":{"en":{"language":"en","value":"When is a formula a loop invariant?"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6481941"}},"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":"Q2945711$38225442-6A51-4C8E-9480-74D64DB0647C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5dd4ee2804ac576db06fb8922a7e10ddec247921","datavalue":{"value":{"text":"When Is a Formula a Loop Invariant?","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2945711$C4094383-C35B-47E7-A527-DEAF200B4C43","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8cfc62597471d742f3b15f6b898502380501ca28","datavalue":{"value":"1321.68191","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945711$D45CAC4B-98DD-40E3-9110-771374A051A3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9187596a066c43c3a3aeaeceeb89f9a3c0680a32","datavalue":{"value":"10.1007/978-3-319-23165-5_13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945711$B28EE624-DF45-4AD7-8920-B00F82990635","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4884ea388d9a1b061adeca7a34ce809061266cfb","datavalue":{"value":{"entity-type":"item","numeric-id":877835,"id":"Q877835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945711$D83CA879-9530-4F8B-950C-AE0F10A9EEC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7a60a38320311da18eda10821922742954865726","datavalue":{"value":{"entity-type":"item","numeric-id":394492,"id":"Q394492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945711$44C28949-332E-4807-965F-7C0A116C502B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945711$507B4F7C-AF0B-4E26-A512-AA685496D98E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ece460bc202bb4ec344b5d620998e472753b138b","datavalue":{"value":{"time":"+2015-09-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2945711$14B2FC5F-BD2B-4A6D-93A5-C0F1B18E3093","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945711$01F445BF-389A-483B-8DC5-3A167D29E29B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"09ff32d05aa3e2b17e796c67b742635d27d31708","datavalue":{"value":"6481941","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945711$70541422-F66C-4B72-959B-035FE624662E","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":"Q2945711$C3F95589-7B50-43CA-ACAD-AA32EF93D5EF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5c0287f49445cb809772e6190e448c16ca22c20a","datavalue":{"value":"https://doi.org/10.1007/978-3-319-23165-5_13","type":"string"},"datatype":"url"},"type":"statement","id":"Q2945711$E5C655F3-874C-4B35-B329-147A631C0454","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ab6cd14f9d14b4fec8bf3dd5f9e39a6d8fedca67","datavalue":{"value":"W2286020247","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945711$5AEE9927-B077-46D0-B772-EB333F552D43","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"48c2c388a22640ac9d5b19d2053fe4b933139852","datavalue":{"value":{"entity-type":"item","numeric-id":5172647,"id":"Q5172647"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945711$4E56688B-49CB-4188-8F6A-9E23C9477CE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ef9a85754f10c794d7ea794155cce4bd2f066956","datavalue":{"value":{"entity-type":"item","numeric-id":3075471,"id":"Q3075471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945711$BF76FE31-971C-488A-B027-7B99E2E38FE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc3406683ad00aa9363d90c4954863b73476c44d","datavalue":{"value":{"entity-type":"item","numeric-id":2843317,"id":"Q2843317"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945711$AF3C071C-9964-47FE-9DC2-9832D2081596","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b33761cd4c211b18999de7cfdb3091c2417ed5f","datavalue":{"value":{"entity-type":"item","numeric-id":3525138,"id":"Q3525138"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945711$89489EB4-5BA0-4BCC-BC80-4A9BA8A47017","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bcdd88c0187437df1dd77abdaba504f2664c711b","datavalue":{"value":{"entity-type":"item","numeric-id":939166,"id":"Q939166"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945711$71606F56-1F09-49D6-9A30-50E6A2E26E08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2ff57ef70bd9e86c9b7017e46b8cd84cb7965f4","datavalue":{"value":{"entity-type":"item","numeric-id":3714165,"id":"Q3714165"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945711$363FC2FE-3209-49F0-8E15-01F4925ED0D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf7e5ea8b887807f5a5d06a897412368d42a81e7","datavalue":{"value":{"entity-type":"item","numeric-id":5245268,"id":"Q5245268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945711$A3475BF4-A56C-425F-A562-A5AAD1742ADB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"358a4e09d6cbdccb0a6a97551bee24c6efb9d080","datavalue":{"value":{"entity-type":"item","numeric-id":5326338,"id":"Q5326338"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945711$B9422A96-C839-463A-B9E5-6D2E06CDB063","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e29a9e63db651327a88d88e2cdc75e51e9cd4afb","datavalue":{"value":{"entity-type":"item","numeric-id":2843329,"id":"Q2843329"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945711$31764F9D-CC0D-4257-BAC6-72A3D4778AA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66f1b17812e6037d2b7d557b0a7606920332b887","datavalue":{"value":{"entity-type":"item","numeric-id":1124373,"id":"Q1124373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945711$CFB62945-A64F-43D2-8D2A-DFCFAEB0AB61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"479a9e80b567553c1d8b3d175d25ba4c9879d09f","datavalue":{"value":{"entity-type":"item","numeric-id":882517,"id":"Q882517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945711$AB296E7A-DE0F-48EE-8944-6B4F64EEC4DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9746a3a7577f68c17412e51cb034688f80cc2301","datavalue":{"value":{"entity-type":"item","numeric-id":5166700,"id":"Q5166700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945711$EFAC86F3-6249-4F01-958D-9C4CF91BF807","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d79f794cb0b04265fbc6f7edbeaedf1dc142dec9","datavalue":{"value":{"entity-type":"item","numeric-id":5308685,"id":"Q5308685"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945711$C118F4BF-19D4-4604-B228-AB1DD08FD8B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7fcf2296969dd5e01651c8f2a620352248abf9ef","datavalue":{"value":{"entity-type":"item","numeric-id":5308375,"id":"Q5308375"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945711$8B161C6F-5C8E-4FCD-A943-37176A48A2A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9c89dbab3e6b723e605c6aa70dd1a0838f12ee2f","datavalue":{"value":{"entity-type":"item","numeric-id":859956,"id":"Q859956"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945711$1C4085B6-2566-4199-A80B-86F19BC23834","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ac80f8dd6b9c81d89f3e2f783c850787d622bd9","datavalue":{"value":{"entity-type":"item","numeric-id":2457430,"id":"Q2457430"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945711$1418BB23-D6DB-4152-ACA4-8970F6C48958","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3859466e501b97ebc1c0602831ac1db9d4b9c730","datavalue":{"value":{"entity-type":"item","numeric-id":394493,"id":"Q394493"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945711$7F0346EC-BF8A-40A8-994D-7F0E8211E344","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c0c4a4d094397169a2c326dca542cfa014ddbe4b","datavalue":{"value":{"entity-type":"item","numeric-id":3392933,"id":"Q3392933"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"444984f33335f6dc5dda47c60d70456e4617afd1","datavalue":{"value":{"amount":"+0.7832620739936829","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":"Q2945711$066250DF-C166-4009-81E9-7145E13AFA7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"25ac48785266b934049e115a22c29640cef3fafe","datavalue":{"value":{"entity-type":"item","numeric-id":3698287,"id":"Q3698287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0b0271c9e0088bf560788596d20c508c9e5e3d88","datavalue":{"value":{"amount":"+0.6876310706138611","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":"Q2945711$5078F67B-8497-420F-87D2-78F0ACD4CD68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"08b60e9fb652d1d68d74657911a8caa315e4c123","datavalue":{"value":{"entity-type":"item","numeric-id":394493,"id":"Q394493"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bea671f0f9a89d77e09f06f405494d7f196d8342","datavalue":{"value":{"amount":"+0.6870949864387512","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":"Q2945711$89262160-2DAA-4572-B37C-E4449777B1D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ecf08f9e6eae6c33e54be636f8491d559294d6d6","datavalue":{"value":{"entity-type":"item","numeric-id":3004678,"id":"Q3004678"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"49c0c4e2325a6005db49c37b32c086af7457e351","datavalue":{"value":{"amount":"+0.6839818954467773","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":"Q2945711$C77878BE-000A-43F9-8333-FE7AB0261539","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"10a03ae8828793c7246794c737052e077fcac13d","datavalue":{"value":{"entity-type":"item","numeric-id":3637252,"id":"Q3637252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c131b7500362bbfe085b6ae60bff759091cf2f9d","datavalue":{"value":{"amount":"+0.6738559603691101","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":"Q2945711$A0F66C38-1033-4CB2-B4A7-9E24565E7E1C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"When is a formula a loop invariant?","badges":[]}}}}}