{"entities":{"Q3646570":{"pageid":5676476,"ns":120,"title":"Item:Q3646570","lastrevid":87688550,"modified":"2026-06-04T12:21:40Z","type":"item","id":"Q3646570","labels":{"en":{"language":"en","value":"Automatic generation of non-linear loop invariants"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5636750"}},"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":"Q3646570$2E59AC2E-572B-40AC-90F8-C64D17AA7E7C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"60f16b47e581993f75d185ca3d62ae19dda5464f","datavalue":{"value":{"text":"Automatic generation of non-linear loop invariants","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3646570$345EDD1B-74CA-431B-9703-DA540169879F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"70bba083a95c4af1fe28b2181937481ec467042b","datavalue":{"value":"1175.68263","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3646570$4131B0AE-FCC9-4D5C-9373-952E24BF77A2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1ef27ab69ff13b051a35f7717525e150201d1b8e","datavalue":{"value":"10.3724/SP.J.1087.2008.01854","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3646570$B158CA4F-FAEC-4344-BDDA-6AF0983A904C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e568b81e8e4204fed4451187a9faf3e33566aece","datavalue":{"value":{"entity-type":"item","numeric-id":2949603,"id":"Q2949603"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3646570$86481BBA-FE68-4E46-B791-0FAB1C6E266F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bbcf9ac1ba76a06a48faf533f4bb13c409546036","datavalue":{"value":{"entity-type":"item","numeric-id":450300,"id":"Q450300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3646570$77375036-2880-4E36-942C-ADA143312B13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4c452427a157200cf37c0b4c875f781889bdfd00","datavalue":{"value":{"entity-type":"item","numeric-id":3185473,"id":"Q3185473"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3646570$5855E8E5-B649-4F35-832C-657463EEE40D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3dd0f4a863078e32a4c218c26f3bff7cf9c6f1a3","datavalue":{"value":{"entity-type":"item","numeric-id":2844978,"id":"Q2844978"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3646570$E1BF4C6A-3A2A-45D9-99AD-B519EC90F07B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5c9bdc6b8e381e5a43d07aa231753eb35d8e55b7","datavalue":{"value":{"time":"+2009-11-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":"Q3646570$6A3949EC-3DA7-4C1B-A127-39D37242211D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3646570$41156EF6-0F3E-4DD0-93A2-F973B9B8F029","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8f412c62952107f7ff74e77578c2ab25d3e121a","datavalue":{"value":"68Q85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3646570$0BFCDA95-5095-46B3-AF31-C047C2B3841D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d703613c1c0089da0ddca8a79695b7770550e019","datavalue":{"value":"5636750","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3646570$D042637E-6F8A-4D3A-85DC-31AFF6ACEE48","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q3646570$2095503A-158A-49AA-8C5E-8592397AE612","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fa0a4da572274ad55899bfb2fae87dc4ba0cbad2","datavalue":{"value":"loop invariant","type":"string"},"datatype":"string"},"type":"statement","id":"Q3646570$A9CEF5A2-0BC7-4E7A-AF4E-8F0799A977C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d9408546ecb33d5fe54dbb1dbe82b7a513b60f62","datavalue":{"value":"transition system","type":"string"},"datatype":"string"},"type":"statement","id":"Q3646570$CB630571-DAE3-44B1-AAEA-C07C683A4A7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f025237192ea9650da6e9ea221af3d52a9614e9e","datavalue":{"value":"constraint solving problem","type":"string"},"datatype":"string"},"type":"statement","id":"Q3646570$EE2D3D92-48C3-427B-92E8-8543465D44CB","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"485f54a0549a89232924cb0abb443c2fad36af9f","datavalue":{"value":{"entity-type":"item","numeric-id":13300,"id":"Q13300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3646570$1EDC288F-6867-4428-B814-41C537605AA0","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":"Q3646570$E8B400DB-E5B3-4043-837F-3AF327E4B4C6","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e44f84f769f4f9ab334f19fa186dc1ad89ccad58","datavalue":{"value":{"entity-type":"item","numeric-id":5119943,"id":"Q5119943"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8093122439b3954fce0f1c26ae6f40f8eb611b76","datavalue":{"value":{"amount":"+0.92982733","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":"Q3646570$7BE50FE4-9557-45DD-812A-B79E72A98055","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2f00209fd89c10cc4c8264b757b15d4637ae4628","datavalue":{"value":{"entity-type":"item","numeric-id":903492,"id":"Q903492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fff9fd44efdb9674a6f723cf08f4a0701b2f04df","datavalue":{"value":{"amount":"+0.903542","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":"Q3646570$6321599D-BADA-4934-A94F-80E4A02A7221","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0283527095000a0833b5ae629a19396977be1ccc","datavalue":{"value":{"entity-type":"item","numeric-id":1391929,"id":"Q1391929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0332bf752403106911f8b404f3d9c3ec21085460","datavalue":{"value":{"amount":"+0.89552593","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":"Q3646570$4B749646-0426-4103-B0A4-3599FFA70A84","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":"57509b3c99d3b17825ab92debabf68a10f2dbf83","datavalue":{"value":{"amount":"+0.89482653","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":"Q3646570$BEED2B9B-2B19-4A8A-90DA-A5C387AF42FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e36f3694c49ffa7483df2a818342d806f5dea076","datavalue":{"value":{"entity-type":"item","numeric-id":5740643,"id":"Q5740643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c394b7c52465e9f704c687fbf7485d087d9faad8","datavalue":{"value":{"amount":"+0.892961","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":"Q3646570$5DAE67BD-6473-4C58-8B9B-C68F0C92A9C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a8242cb23154939e3c7ada1e404fda49d2e0e93d","datavalue":{"value":{"entity-type":"item","numeric-id":3297595,"id":"Q3297595"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2c5a4cb7ffd85ab75201c7da91fd65f826a53626","datavalue":{"value":{"amount":"+0.8848526","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":"Q3646570$59AC285A-3B2D-4B74-95F8-9A81BE5C3675","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"55e1ac102e88017aeca9570343676b61175a152b","datavalue":{"value":{"entity-type":"item","numeric-id":4657335,"id":"Q4657335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"888a6fcfc695577907eb0bf2a43c1e11b94a9fd4","datavalue":{"value":{"amount":"+0.8814029","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":"Q3646570$DFC006BD-CFD9-4CFC-9E36-B50D3D08B24F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9cb466b9ae8ef59dc8c7c5d5df099f614b41338d","datavalue":{"value":{"entity-type":"item","numeric-id":3416386,"id":"Q3416386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"93fba085230d1955c501723bd82bd0c60d236f16","datavalue":{"value":{"amount":"+0.8805561","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":"Q3646570$4A82AC74-F6BD-4840-AC09-9FCD10F51D47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"76b63caf5f28b762bf948547dcc600d322ce5750","datavalue":{"value":{"entity-type":"item","numeric-id":2180218,"id":"Q2180218"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3aa4e4b94d9e60c453bce7e3e9d0a85f69241739","datavalue":{"value":{"amount":"+0.87727433","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":"Q3646570$C1C9AB8B-C542-4387-A8FA-706C59C029B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"176aff1888dfe6f5e59fd7e5deb833fd7342adfb","datavalue":{"value":{"entity-type":"item","numeric-id":3452270,"id":"Q3452270"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6366c78878ca0d7ccd102ad90cc464aaeb579d87","datavalue":{"value":{"amount":"+0.87649536","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":"Q3646570$67742DAC-AFF3-4DE2-84BA-E958EEA298C5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Automatic generation of non-linear loop invariants","badges":[]}}}}}