{"entities":{"Q5233241":{"pageid":7262809,"ns":120,"title":"Item:Q5233241","lastrevid":41891288,"modified":"2025-05-09T11:36:38Z","type":"item","id":"Q5233241","labels":{"en":{"language":"en","value":"Loop Invariants from Counterexamples"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7105463"}},"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":"Q5233241$B51B6EEA-2F6A-41C4-B7B9-61737E737981","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c0e7cde476eed9d626f5b338ad557d3a2134e89f","datavalue":{"value":{"text":"Loop Invariants from Counterexamples","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5233241$96C3FC4E-DFCE-4D40-92E4-658364665F0D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"bdfdb7b68e0181f1f174581b47e349e252cfc220","datavalue":{"value":"1420.68128","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5233241$F7B27222-2CB5-41A8-A943-10E4A8475C3A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ba4c7cd7fb7f1d60bdf8fed026bbbcc6d39e5e74","datavalue":{"value":"10.1007/978-3-319-66706-5_7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5233241$3577AB18-D200-4BEF-BF57-7A527713AA62","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"acecf5d1a92854cd265cb9f612b3c2aedc979552","datavalue":{"value":{"entity-type":"item","numeric-id":2988929,"id":"Q2988929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5233241$9D4E158D-6AF5-4F87-A726-9E83D5C748CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"82e156e8fa4d3f1d15652d6c661fd72d146102a7","datavalue":{"value":{"entity-type":"item","numeric-id":1629965,"id":"Q1629965"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5233241$C5D81D58-3429-4E2B-9B13-FA408EFFDD6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3527a91821d36e757e1613c0da59458b564b0344","datavalue":{"value":{"entity-type":"item","numeric-id":225062,"id":"Q225062"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5233241$1920E2BE-C23E-45F5-AB21-463AE5D42971","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"19e166a297e557c212f7b597bbbbc3f69b1ceb4f","datavalue":{"value":{"entity-type":"item","numeric-id":2870767,"id":"Q2870767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5233241$0B2C1062-BC0C-4C3F-B8F7-6E16ED2DB153","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"96391af82153a94a4af2a0e4c8ac60042cea1674","datavalue":{"value":{"time":"+2019-09-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5233241$6122E01D-3111-4674-95EA-08E7267B14FA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5233241$09421DB5-5F5B-423C-AF99-7F3E333D6A7A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9e164fa79d5f363abbe3cd639d43ca3359a8cc2a","datavalue":{"value":"7105463","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5233241$DEEBD417-C829-43CC-B2AA-3CB94F8F3A17","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c25e2917fa8933db2dcdfdde3120016ec3860077","datavalue":{"value":{"entity-type":"item","numeric-id":35079,"id":"Q35079"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5233241$852043DF-F528-4EAF-86C2-7D76DFD33DFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2c47fe2df1f1953bad823a45d5770cd3dadc8780","datavalue":{"value":{"entity-type":"item","numeric-id":19438,"id":"Q19438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5233241$570F52CF-D093-41A6-A8AA-4F9BF45D5E1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5233241$E281941E-1357-4038-ACC6-EB63CDF09DF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a1d6b9e920f2e41a66a9767e31ca972ed7628dde","datavalue":{"value":{"entity-type":"item","numeric-id":15668,"id":"Q15668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5233241$9248309F-76A9-4B9A-99E0-32DBE19131EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e1655b290b91a673f0538ce14f6694f64d961977","datavalue":{"value":{"entity-type":"item","numeric-id":19440,"id":"Q19440"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5233241$57EBCDB1-CC01-4819-A274-B66032F416F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bd3fa568ce44545ce1c1bded3c45ecc37b43b7c1","datavalue":{"value":{"entity-type":"item","numeric-id":21467,"id":"Q21467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5233241$5B5A16AA-B966-4871-8958-5C8443EDDD58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a4f636583a26240d6177ac1ea0a1a2046a522c7b","datavalue":{"value":{"entity-type":"item","numeric-id":21551,"id":"Q21551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5233241$0FFD2F5B-C8BE-4981-A289-E4E24AFE43DE","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":"Q5233241$D5CC97B7-AEDD-480D-A8C7-454AC424E74E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2d7324473e104b22a84f09990937dc3f1fb46100","datavalue":{"value":"https://doi.org/10.1007/978-3-319-66706-5_7","type":"string"},"datatype":"url"},"type":"statement","id":"Q5233241$6D854770-826F-4922-99BF-EA55966C482E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b8e7beb916655e434bbc58bf8dbdd82d78282ed7","datavalue":{"value":"W2750327884","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5233241$25C6D557-D85C-41D0-B292-50AC1F80B5F1","rank":"normal"}],"P1643":[{"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":"9255510b0a9478a14e31c419ab4354fd8b68a910","datavalue":{"value":{"amount":"+0.9084823","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":"Q5233241$9FE59966-4611-429D-B39D-1CB0050F6A05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b94c01cd18d6403d2f48321e57b93a16d34b8618","datavalue":{"value":{"entity-type":"item","numeric-id":5493379,"id":"Q5493379"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"15e99f1248f7b74e0e5f488816f23f6e5087f5d5","datavalue":{"value":{"amount":"+0.88742656","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":"Q5233241$928AC750-7962-4C97-A50B-EF94C5FB37A9","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":"9785d612f20bcedf9dbb8f9017e1b06148ff2514","datavalue":{"value":{"amount":"+0.877112","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":"Q5233241$AD3F157F-7204-46B7-BD79-259CD8B4275D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9b2926bb22504cc84dd44c32153de12a2f8f517e","datavalue":{"value":{"entity-type":"item","numeric-id":5738909,"id":"Q5738909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1cb937901e41b7223f48818d9dc81a2b0218ea96","datavalue":{"value":{"amount":"+0.86748666","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":"Q5233241$E7403E47-2D23-4C62-8E59-94BDCF066A0F","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":"ecdc0f99cf8edb6c72a5f8d970ed2983bb89880a","datavalue":{"value":{"amount":"+0.86541474","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":"Q5233241$866049B5-E493-4ABC-89F1-980D811BB992","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ba35208f62cfccec59b23a3ffcc5b718ee7d7c7b","datavalue":{"value":{"entity-type":"item","numeric-id":771839,"id":"Q771839"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"15246b56b3f15ff8ee56179a27f01c2afbac327b","datavalue":{"value":{"amount":"+0.8617469","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":"Q5233241$B34D6542-7361-4A0E-AC51-650422A50044","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b1496f2261ef40b96f7f6eb612c79f133a951e38","datavalue":{"value":{"entity-type":"item","numeric-id":6164420,"id":"Q6164420"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6287f9dbcf4e83c68403c1c8914f7e04276e6993","datavalue":{"value":{"amount":"+0.8586166","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":"Q5233241$AEF3B9DA-3B3E-4B88-AEC7-A1B128E94ADD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f464b64c5ce744bcc9e044bb866ec7efefd38317","datavalue":{"value":{"entity-type":"item","numeric-id":604381,"id":"Q604381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d16a6ab7c6c6ccc4045c6fff53bab28b9a633b83","datavalue":{"value":{"amount":"+0.85856456","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":"Q5233241$7D3D2C08-8807-416F-AC39-1C8468437EFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"74f1ab42347132194a4620ab8227caf321ce7cc3","datavalue":{"value":{"entity-type":"item","numeric-id":3585023,"id":"Q3585023"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3ae66f7999d35dc373709e1e3b9dbffda8ee7fb5","datavalue":{"value":{"amount":"+0.8582808","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":"Q5233241$CEA9B18C-1637-4D04-A6D4-9BFB08CF73B1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5233241","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5233241"}}}}}