{"entities":{"Q2233530":{"pageid":2244273,"ns":120,"title":"Item:Q2233530","lastrevid":43733844,"modified":"2025-11-11T10:56:11Z","type":"item","id":"Q2233530","labels":{"en":{"language":"en","value":"Predicate abstraction and CEGAR for \\(\\nu \\mathrm{HFL}_\\mathbb{Z}\\) validity checking"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7410588"}},"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":"Q2233530$FCB86648-B996-4836-A68C-C6C06D02DB53","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0b26b36a60f3891fb29115122a22ec5aa9bc0e9a","datavalue":{"value":{"text":"Predicate abstraction and CEGAR for \\(\\nu \\mathrm{HFL}_\\mathbb{Z}\\) validity checking","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2233530$1DFFB478-DAF8-4A31-9311-D1B9CF673D55","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2a5ab171c1e26aa12e5495c3b55faf8abf84cade","datavalue":{"value":"1474.68190","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2233530$9EE1B46E-5651-41CA-B7BB-2B94140A7518","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8c22c8522ef6f302c8c601d4a238fd807cd588f0","datavalue":{"value":"10.1007/978-3-030-65474-0_7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2233530$A2A37060-A493-48CB-8859-E0CC3B1A29D4","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8cb7012016010ddfde30b5c590c6aa5231106c2e","datavalue":{"value":{"entity-type":"item","numeric-id":2038068,"id":"Q2038068"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233530$114FE0B7-186F-4B71-BD83-D803ACF62791","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e3ed03c0e908613601fdd733dba97c4f4513b0a5","datavalue":{"value":{"entity-type":"item","numeric-id":238500,"id":"Q238500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233530$BB5C8AF2-0421-4AB1-8EC4-42EBC0AB2D43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"17cfd53e5e61b75272cb083cb1d597ccd84c9e71","datavalue":{"value":{"entity-type":"item","numeric-id":2233529,"id":"Q2233529"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233530$841DF35B-CE6F-4FBA-B019-156581C76E1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f0eaf951c75d2d5db5073cd2949ee5f4196ba23e","datavalue":{"value":{"entity-type":"item","numeric-id":2038069,"id":"Q2038069"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233530$39F81820-F0EC-438C-AB7F-DF2DE8370DDB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"899d672926fe97cd87f3708d91dc74172e4f3b51","datavalue":{"value":{"time":"+2021-10-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2233530$CD0B6948-AAEA-43F5-9AF4-D6754919AA7F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2233530$DE38E9D2-937A-423B-9140-AE0294CE3FF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2233530$171F2DD4-C241-4B8B-B141-4F36095B8E77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2233530$B47EA5DC-8C21-4FCE-A216-7D89500B84B4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"52e7ec3ee675b33535a4d2bc4e69229aebae0ed0","datavalue":{"value":"7410588","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2233530$3DF47621-B501-4321-8589-A674F0535CF7","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":"Q2233530$40DF6083-C27C-4245-9FCC-E01627AFC5D3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"09397a4a5a59f28aec93ddc086a16dfd03d7c1f3","datavalue":{"value":"https://doi.org/10.1007/978-3-030-65474-0_7","type":"string"},"datatype":"url"},"type":"statement","id":"Q2233530$AFAA33AD-2B67-4C51-A5B5-3700972EA9E5","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"36f07f6456beb1fd96e84a996358363164d24a96","datavalue":{"value":"W3120672074","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2233530$D86A98AF-7D4C-45B8-91A7-3C20F2A397C5","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"dc85e7648787a5ed94053adc1ecf581a9fa4439a","datavalue":{"value":{"entity-type":"item","numeric-id":5919615,"id":"Q5919615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233530$945C071B-D50D-417A-9699-800455990FAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cd8212d1e6f4937780f720da0b507691399bd2db","datavalue":{"value":{"entity-type":"item","numeric-id":5370859,"id":"Q5370859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233530$33138BFD-45B6-4AC3-8D57-0A7EA07314B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e00578bad80a34483e52f8ce9687dcb6d88fcf9","datavalue":{"value":{"entity-type":"item","numeric-id":2324003,"id":"Q2324003"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233530$686D5479-A7F9-4155-A9DE-188088C135A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a18b608fd7c828c13168c46a5c81fbf400275ac","datavalue":{"value":{"entity-type":"item","numeric-id":1702897,"id":"Q1702897"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233530$471CC56C-C842-4033-A2A3-7FE28EB2BA64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5b8d9876fc4b1bc762aaa2e76ab4503f7e596a90","datavalue":{"value":{"entity-type":"item","numeric-id":5255067,"id":"Q5255067"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233530$799F4D45-4AB5-4144-8113-CB6F3A5922FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d44484491b105b4eba9052e7ca901f22afe79de5","datavalue":{"value":{"entity-type":"item","numeric-id":5311496,"id":"Q5311496"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233530$F3E04DA5-DAB6-4F2D-B02B-30C8AA0A4BE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dcb216eaea9ef5909bc774221bd6070ac3f48525","datavalue":{"value":{"entity-type":"item","numeric-id":2926649,"id":"Q2926649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233530$68E6904A-7626-4A53-B9C0-FC8E128D7703","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"abee67a4a5c18c8985c4b59db7ff0c63c1633c05","datavalue":{"value":{"entity-type":"item","numeric-id":2981992,"id":"Q2981992"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233530$B6A4CE73-69DE-42B4-9A1D-046E0B00ECBE","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4599161c3141d41b963eaee6a517f0cbf62f4ecb","datavalue":{"value":{"entity-type":"item","numeric-id":2038070,"id":"Q2038070"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"274bbc59b690d7dda346df71c04900eebf77e0f1","datavalue":{"value":{"amount":"+0.88743997","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":"Q2233530$BD365E7D-1866-4879-A103-0C1772DB3DE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3fe49159c046efa21dd3b33c0a71aaf59869bd61","datavalue":{"value":{"entity-type":"item","numeric-id":1702897,"id":"Q1702897"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0caf3f9b9d5b4d2a05c7418df6b2433317928323","datavalue":{"value":{"amount":"+0.86140203","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":"Q2233530$A735637A-C4D7-465A-A311-BF4498E83B27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dc000ee24b325f01dec0f4b2a1fa6154b4836893","datavalue":{"value":{"entity-type":"item","numeric-id":2369884,"id":"Q2369884"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"50281d0c202f11b82b4249c4d3f6f697e1a360ad","datavalue":{"value":{"amount":"+0.85373354","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":"Q2233530$D9214CF1-D116-4693-B8F6-5F586F9FDB92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6ba55ee38a99d46604b9b2feddb9efbde5b9b1bb","datavalue":{"value":{"entity-type":"item","numeric-id":5240105,"id":"Q5240105"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7a80cef08cfff96d0d9c9b5599e66cdd54813d59","datavalue":{"value":{"amount":"+0.8447134","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":"Q2233530$0484B555-0EA6-41B2-AF23-5B75CD706B30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7bac9d4d28f254e49858c9874367df8c34d82c78","datavalue":{"value":{"entity-type":"item","numeric-id":3176373,"id":"Q3176373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a925e3b2d29d39bbd3c2d80facd78fd3d29cb92b","datavalue":{"value":{"amount":"+0.8440318","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":"Q2233530$F1A85DF8-67BE-4224-B45A-643849B6C8F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ee9691043fc2fa83f9bcad490e83cd2b178847bf","datavalue":{"value":{"entity-type":"item","numeric-id":1987736,"id":"Q1987736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d5709d6cbc93fa8933020b10e7f16bfe2ae71ae9","datavalue":{"value":{"amount":"+0.84380674","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":"Q2233530$E3F9A65E-4492-49B1-92B7-00ED34F758F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bd9561e57bdeae0bb9b06717d09bad3b2edf754c","datavalue":{"value":{"entity-type":"item","numeric-id":1961429,"id":"Q1961429"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0a70f9ac266bfb7c9655fdddaf6c245bcdb5cf85","datavalue":{"value":{"amount":"+0.8427093","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":"Q2233530$8C4B878A-9ED9-4DC1-9669-066D3524B536","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bb6b0c7708aa1b29fb28822785bf693edde31f9b","datavalue":{"value":{"entity-type":"item","numeric-id":5312923,"id":"Q5312923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cbf2817dda971331a56752e31cdec903550f0a19","datavalue":{"value":{"amount":"+0.84219813","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":"Q2233530$1522C8AB-606A-44DD-AD7C-0753B72AFEF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fbbea5b26860a93d5fef730d8f8a1451daf10bae","datavalue":{"value":{"entity-type":"item","numeric-id":4808810,"id":"Q4808810"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"40278c162a054350d6923fb4e53ed8434b610b30","datavalue":{"value":{"amount":"+0.8410059","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":"Q2233530$C894CC61-25F5-44CB-9A9F-8CA87D5CA5DF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2233530","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2233530"}}}}}