{"entities":{"Q2044196":{"pageid":2054938,"ns":120,"title":"Item:Q2044196","lastrevid":57707622,"modified":"2026-04-01T00:32:11Z","type":"item","id":"Q2044196","labels":{"en":{"language":"en","value":"Counterexample-guided prophecy for model checking modulo the theory of arrays"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7378300"}},"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":"Q2044196$A7C825D0-68E3-44D9-9676-0E65A1D368DD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c9775176a59c2480da825b8f4d9efa8e67a80173","datavalue":{"value":{"text":"Counterexample-guided prophecy for model checking modulo the theory of arrays","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2044196$27F1F974-7741-481A-945B-1F988DCBC439","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"814e96cae706c202f42bac1aa63fec04dc8245d5","datavalue":{"value":"1467.68089","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2044196$8F9800FD-A0E4-44A6-B842-8EF29BC79D14","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2210be0ca33efa9d3f18a6188a0bd41badc38d9c","datavalue":{"value":"10.1007/978-3-030-72016-2_7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2044196$083661E1-5B53-4416-BD49-3CEC4E0ECD55","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"eb4f6ec7d4f100918fa8e18eefd60720c243c468","datavalue":{"value":{"entity-type":"item","numeric-id":2044194,"id":"Q2044194"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$EA3ACB24-1B5B-4656-A496-097A4403C18F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"637b63b8551b0d9a45289b2321fc07fbecec8861","datavalue":{"value":{"entity-type":"item","numeric-id":831940,"id":"Q831940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$4B76386C-9525-4199-B7F0-6F9323799803","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e97e7d65eece04188cb1a1dff66ddc09c38fbea4","datavalue":{"value":{"entity-type":"item","numeric-id":479835,"id":"Q479835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$C3450C51-EB78-4770-B0CD-AE5CDD5BDF4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"af28c01640955d451ab13d8ae854a3ea0fd656ad","datavalue":{"value":{"entity-type":"item","numeric-id":2044195,"id":"Q2044195"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$4424798F-7023-4A76-AAAE-B7E547E369DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ad77f9f95b13763d1bf3e18f3ef5b6900b795f74","datavalue":{"value":{"entity-type":"item","numeric-id":518400,"id":"Q518400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$A4C862EE-8976-4E3D-A450-AAE8B95B25B1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6f25f924676185979ab6f246b476dde833797f44","datavalue":{"value":{"time":"+2021-08-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2044196$133DD019-2C33-48F9-B399-E2D637B555DA","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fbada17810e0f21b67ade134d53912bb9d3d59b3","datavalue":{"value":"https://arxiv.org/abs/2101.06825","type":"string"},"datatype":"url"},"type":"statement","id":"Q2044196$509062C1-F92F-4BC2-98B9-3AAB5E12407C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2044196$84B39CC6-44F9-4F9E-A47C-50728AB29741","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"46521eb877c5b1eb95ff0bd88248b918be49c5d5","datavalue":{"value":"7378300","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2044196$F6F3A478-43A0-4175-A7EB-81ED93685C01","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":"Q2044196$F17030DE-0888-4017-AF4B-9850A9FE8D40","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f51a2887f09bc4e241dc94fcf080bd1d2da8d96c","datavalue":{"value":"W3148335769","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2044196$3D21FA5F-746C-47D7-9552-989BA04E060A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5d5978f4bdf14ef5fd8b71ce390dbec5034a1e6","datavalue":{"value":{"entity-type":"item","numeric-id":805251,"id":"Q805251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$B30AB52F-2B31-4BD5-A756-C57E5C1AC408","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6a257ff0958ba2ab18651e0ae0e647b82a1a678f","datavalue":{"value":{"entity-type":"item","numeric-id":2891439,"id":"Q2891439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$A007038B-DD12-4CCB-BB39-CAB44C622E2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f176d988fabbd626744eee2651f4ef8cf9c0825f","datavalue":{"value":{"entity-type":"item","numeric-id":3457775,"id":"Q3457775"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$79CB7E9B-03E1-4602-A64E-DBE0A41018D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2a5f7ec14119349332290c2a3236ae73e2231fc2","datavalue":{"value":{"entity-type":"item","numeric-id":3176369,"id":"Q3176369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$5C125864-7096-41B7-8645-12BB5BD59DF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2518ba6a38fa213a00f5ef7c14d9debc5928424c","datavalue":{"value":{"entity-type":"item","numeric-id":2947164,"id":"Q2947164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$0C648075-B04C-44B9-9498-8A98D1266B59","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":"Q2044196$7A177B2E-08DC-432A-8621-C1C739A6413A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f2b1ebc1ae7ffc3042b5e838a24da8662374478","datavalue":{"value":{"entity-type":"item","numeric-id":5898633,"id":"Q5898633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$4BE21421-86A2-49DC-8679-4F1C151A3419","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5d4d5df30bde2099983c3bf5f07484cf1031c989","datavalue":{"value":{"entity-type":"item","numeric-id":3181652,"id":"Q3181652"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$67798928-BF98-4BFD-82E7-3385B860358B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a65772bcb5d34897d069e1d69f622e23342728c","datavalue":{"value":{"entity-type":"item","numeric-id":2964457,"id":"Q2964457"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$3E32C02E-F231-4FAC-83BB-72D22117032D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f1645d5977fcbb346c223f2e9f46edf7dc223d58","datavalue":{"value":{"entity-type":"item","numeric-id":4691738,"id":"Q4691738"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$2192F8E0-8C0D-4E9E-97C9-40B527C7E2D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a721eea058e807770cf825065bd252a7ab7056d","datavalue":{"value":{"entity-type":"item","numeric-id":2363814,"id":"Q2363814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$23E2E9D5-352D-4501-B4A3-18996001F88B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"21640ae8e3aa02debe92970cf2184aca918b76e5","datavalue":{"value":{"entity-type":"item","numeric-id":5326318,"id":"Q5326318"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$F97781EE-5150-49DB-B945-FA429CF87BB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f162e20dc2fb76efac3e52f404a7c7a69ba6016b","datavalue":{"value":{"entity-type":"item","numeric-id":2996914,"id":"Q2996914"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$096ABA19-F498-4BD0-A990-B57A322DE219","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6a25409f0a2955ff9227dd74a7c11fe04dac7c5d","datavalue":{"value":{"entity-type":"item","numeric-id":1039842,"id":"Q1039842"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$BD716F15-BB1B-4F70-B879-AA8A205CB07E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8971435217b64c50e375aec68a6c58475d8d0dd9","datavalue":{"value":{"entity-type":"item","numeric-id":3249759,"id":"Q3249759"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$846F89E2-06ED-4233-8449-E2BACCCA1393","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2cdb831970cdc01d205b526f08958ccd77a1ab13","datavalue":{"value":{"entity-type":"item","numeric-id":5747748,"id":"Q5747748"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$3FBC6206-4707-4013-A2B6-EF564EF2E245","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cd51bbb96625374ba0527eef6fa500f596e78094","datavalue":{"value":{"entity-type":"item","numeric-id":6109591,"id":"Q6109591"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$AC7CAB1D-D86D-409C-ADBD-1D5624DD288C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fdc3d259cc7fac0e3bc3d0b896617a58bb7c7d08","datavalue":{"value":{"entity-type":"item","numeric-id":4645747,"id":"Q4645747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$D17BBAB5-BBF0-4A03-ADA6-3E9AE73C9AD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f1060c39f6c78c6c906f6922c72b026efa0999e0","datavalue":{"value":{"entity-type":"item","numeric-id":518396,"id":"Q518396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$AA2CF3F8-68DF-428F-B0D1-351A5078D820","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca74c1b4b01eb5401c8b784be60efc1c72a7ed76","datavalue":{"value":{"entity-type":"item","numeric-id":5312894,"id":"Q5312894"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$E359B7C9-B45D-4896-9B50-B2ECB48284DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb3d973ee67a0d57722d1373dad12c99bf3d07ce","datavalue":{"value":{"entity-type":"item","numeric-id":2044196,"id":"Q2044196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$004C737A-361E-4D35-A6A0-61B2A7C81584","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f1a62c24cddf605dd86a399f231d937d5444e0b","datavalue":{"value":{"entity-type":"item","numeric-id":5458341,"id":"Q5458341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$0A084E7B-E886-45E7-B498-DFAA1AB213F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"281d23eca7aaf6e5c8716bc59f167dc0721ca04c","datavalue":{"value":{"entity-type":"item","numeric-id":6045004,"id":"Q6045004"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$0F942399-D831-4E6E-A678-D94D2150CEEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d7e7a69944a208912cc786a2c8236ca37bc32116","datavalue":{"value":{"entity-type":"item","numeric-id":1664399,"id":"Q1664399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$7010B07E-9CE0-4783-AEF4-866DA2CCEF0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"31c70ca7f57dec1fd3ec22aa924f436369c54408","datavalue":{"value":{"entity-type":"item","numeric-id":5020662,"id":"Q5020662"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$5EF3069E-A8EF-441F-9245-06B158D3808A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bccbf5fc3944a9c4a28f412cecb088c5b82edac0","datavalue":{"value":{"entity-type":"item","numeric-id":5900667,"id":"Q5900667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"51da9db8d432a37f575f29b7d0aec16503e8b091","datavalue":{"value":{"amount":"+0.7899960279464722","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":"Q2044196$5430D559-C81C-4119-A6AE-91845E737EEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cbe651991cbc4916826a09c50dbc4cb815d3f966","datavalue":{"value":{"entity-type":"item","numeric-id":3541687,"id":"Q3541687"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"734111c5b6c282c1b8e9cacebfc94d8dbf0cf3d1","datavalue":{"value":{"amount":"+0.7760026454925537","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":"Q2044196$16F549F7-67A3-4877-9773-F70C21A6F558","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b5374a685b3ad64a9cc08b51af3ff70626b89f79","datavalue":{"value":{"entity-type":"item","numeric-id":5747748,"id":"Q5747748"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4017e898073094985e140dc325715cc5233b1ff2","datavalue":{"value":{"amount":"+0.7479894161224365","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":"Q2044196$D9E9B33A-BCC4-4459-BEF8-B144A8D25A2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7441d0ac138a42ca07544f96589c657fae15c5d5","datavalue":{"value":{"entity-type":"item","numeric-id":5178977,"id":"Q5178977"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"161417e1e7e9aed2ce3ff4d5509ddf5034ce0415","datavalue":{"value":{"amount":"+0.7406764030456543","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":"Q2044196$CABBC7BE-AE81-4655-9AA7-A982DF10208A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"65fd47484c6b00d882d3302f057fc283b851b47a","datavalue":{"value":{"entity-type":"item","numeric-id":4930739,"id":"Q4930739"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4ea2aa11014be32a5d845ec4b5f6c3687a8a4dd5","datavalue":{"value":{"amount":"+0.7346764802932739","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":"Q2044196$1EA5292F-BF6C-4ED0-AD16-1F6E7982353A","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044196$53BF07C8-54E7-41B2-ADF5-51B6C806EA58","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2044196","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2044196"}}}}}