{"entities":{"Q2512818":{"pageid":2523561,"ns":120,"title":"Item:Q2512818","lastrevid":52185563,"modified":"2026-01-21T02:59:42Z","type":"item","id":"Q2512818","labels":{"en":{"language":"en","value":"Automatic proving or disproving equality loop invariants based on finite difference techniques"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6393475"}},"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":"Q2512818$53101FC3-5C86-4AE1-8C1A-315FC2407655","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5b4fb2d262d6bf955b2e81ccf6e840a87461f16e","datavalue":{"value":{"text":"Automatic proving or disproving equality loop invariants based on finite difference techniques","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2512818$05F73783-20AB-4706-8578-5D3460860ABA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"357bf89dd0eb068f5bb8a0ca5bb92c328062b25b","datavalue":{"value":"1314.68284","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2512818$C6E70B9F-2781-45BF-A39C-146534CCAFBD","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c3a9ef8f7bec0a13d9487613ba93e2a9c1034736","datavalue":{"value":{"entity-type":"item","numeric-id":2512817,"id":"Q2512817"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2512818$319398AD-7E35-42F3-BD10-32A00C055C52","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"52fa7d44b58d0511cb8993765bd916aef86052d8","datavalue":{"value":{"entity-type":"item","numeric-id":63092,"id":"Q63092"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2512818$93B1D7C5-E0BF-4D28-BC10-6997E5B651A2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f8075b727d5838f8aeab25ff1bfeb3492229c802","datavalue":{"value":{"time":"+2015-01-30T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2512818$2588EE30-3A5D-4C5D-9B00-902128B63534","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2512818$6201FAF1-A391-4A5D-A84A-2C5A392D01B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2512818$8217A65E-162A-4306-AAB7-6D091FB0F6A9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6dc887c3cb0d8c950809126f41f588b5d45e632f","datavalue":{"value":"6393475","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2512818$32B74B46-C467-40B2-BA86-32F52BDD3FE4","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9d2aa687cef17cd912aad76972cec097c0540be8","datavalue":{"value":"automatic theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2512818$DA7D00FE-6592-4C2A-9632-628D78716148","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"650fcad3ceceac1dfed7e9050c7b10d694884c9c","datavalue":{"value":"equality loop invariants","type":"string"},"datatype":"string"},"type":"statement","id":"Q2512818$70DA2EA4-C769-4595-B0BA-1DDC54D241E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"14e4329d540bcdcacd6d5126fd9a8acab2d4c3aa","datavalue":{"value":"formal characterization","type":"string"},"datatype":"string"},"type":"statement","id":"Q2512818$51C9A4D8-7D2C-4C72-AA0F-095BD9E9CDDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2512818$62F3F235-2A63-4289-AC6C-AC4BB6192110","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"baba0f8e4c1b1f479bec79af9929e7998ff3dfce","datavalue":{"value":"finite difference techniques","type":"string"},"datatype":"string"},"type":"statement","id":"Q2512818$2BBE9AB4-6A45-4910-B690-E8DB9CA27332","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":"Q2512818$C8312025-8362-4CAA-B81C-66DBF4E5D6F5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7cc2447954c2570ac57dc6ed5069e8dfb3bcaae6","datavalue":{"value":"https://doi.org/10.1016/j.ipl.2014.11.006","type":"string"},"datatype":"url"},"type":"statement","id":"Q2512818$F084202D-F0AF-45B1-9601-A517C1BD3AAC","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ca69129cb3b6b69aea05bbae85747570f35f8ecf","datavalue":{"value":"W2010329882","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2512818$22C79B90-7F2A-4C7E-A6FE-D0507BA3BB55","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"de73056366a093e4fafbe59e002acb1cce516408","datavalue":{"value":{"entity-type":"item","numeric-id":4649805,"id":"Q4649805"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2512818$C35714EA-2DCF-42E0-A18C-BEBFBB3EBAF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f642ff66e8539d846927a8f5618916606bbf48fb","datavalue":{"value":{"entity-type":"item","numeric-id":3586008,"id":"Q3586008"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2512818$C4169AE4-6E12-49A4-B678-C922BCDDC373","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d88a4d21f9c10003cdb38349b5ebb6aa4815e0e5","datavalue":{"value":{"entity-type":"item","numeric-id":5458331,"id":"Q5458331"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2512818$0680B1E8-3947-4287-8F77-B2262F7CB356","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":"Q2512818$B9B203E4-F86E-4A65-B743-43069ECF98C2","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":"Q2512818$F5016E8F-9013-4B2A-B2BD-9B56965F0976","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5543be9943ed5afa4e775fa2b368abaa7788d4fe","datavalue":{"value":{"entity-type":"item","numeric-id":5326308,"id":"Q5326308"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2512818$6203F094-C59B-4D03-98D8-6BE362FE253B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"cb58d5ec9322a75b8d96a30f3de2700f5230165b","datavalue":{"value":"10.1016/J.IPL.2014.11.006","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2512818$16F39B87-5937-4437-87A8-C54A97024FF3","rank":"normal"}],"P1643":[{"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":"cbc53beaab35daf61d2602526ccf542a8b021862","datavalue":{"value":{"amount":"+0.7923360466957092","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":"Q2512818$8EDB7A3F-17BB-4D2E-9F9C-D1F3BF5EC9EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cba91a2fa8a38f05d02fe6a811450a3326020603","datavalue":{"value":{"entity-type":"item","numeric-id":5176169,"id":"Q5176169"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"64b668b9178e66bb65511f0a3e39e79913b4c8f4","datavalue":{"value":{"amount":"+0.7621186375617981","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":"Q2512818$D3E5A768-DFC1-4C16-A61C-15D17CF78FBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a6e4251c7d7c8287cb43fb5e0e28c5f0d5fdbdab","datavalue":{"value":{"entity-type":"item","numeric-id":1065537,"id":"Q1065537"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"adff6c5ec6bec5b3f0b7eda12a680ae8872f12d6","datavalue":{"value":{"amount":"+0.7494708895683289","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":"Q2512818$33C7D8A2-18BC-4C15-9015-9BD5333BE09E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"32d3276762406fd5b69340bd3ed4e749c2093b78","datavalue":{"value":{"entity-type":"item","numeric-id":5709984,"id":"Q5709984"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1351fe1cd4d4883b327914a8dc2d004142183a5f","datavalue":{"value":{"amount":"+0.7467120885848999","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":"Q2512818$511B151E-7128-499D-A2FC-AA4C6DD3C6BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5cb23bd8c9cdca6792eabcff20647876a470cc75","datavalue":{"value":{"entity-type":"item","numeric-id":5096093,"id":"Q5096093"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"653965591b455b9cdf982ce28bb7058903278b82","datavalue":{"value":{"amount":"+0.7461252212524414","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":"Q2512818$CA3D43C1-A41F-4953-A521-7ECA5A7D94EE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2512818","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2512818"}}}}}