{"entities":{"Q1702893":{"pageid":1713634,"ns":120,"title":"Item:Q1702893","lastrevid":73808292,"modified":"2026-04-14T17:19:37Z","type":"item","id":"Q1702893","labels":{"en":{"language":"en","value":"Counterexample-guided quantifier instantiation for synthesis in SMT"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6845633"}},"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":"Q1702893$D49C64C3-5981-4856-9E9D-CCB7F63CF362","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a6771af88b8ff199ef6ebb6f252613d33c909faa","datavalue":{"value":{"text":"Counterexample-guided quantifier instantiation for synthesis in SMT","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1702893$98D34DB5-043C-4B50-B9A8-1CBEAB18B946","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ef016e5fd636abc49f72ef6130f6c9c710f3247e","datavalue":{"value":"1381.68059","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1702893$8D66026A-DDFF-4BC3-A0A8-519102D41248","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5613e639ae9b5d61daa5cff73942e8228a4c57a9","datavalue":{"value":"10.1007/978-3-319-21668-3_12","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1702893$D7775FBE-66DE-4BA0-9C50-D4101CC14B08","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"84952d23570c02a49b2cbd6b6731071617699380","datavalue":{"value":{"entity-type":"item","numeric-id":518398,"id":"Q518398"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1702893$318C805A-A036-41A4-BE5B-1C01C2B98343","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5374aaae6c4fa00723de88e8acb31ca46f3aaf1e","datavalue":{"value":{"entity-type":"item","numeric-id":518401,"id":"Q518401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1702893$26098702-8E2C-4B12-B4D5-B73A633A69BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9c4a981688ce96064434c07429a9f8191c6df21c","datavalue":{"value":{"entity-type":"item","numeric-id":746766,"id":"Q746766"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1702893$EEABD9DF-E5D6-48C0-99C0-89D8EE8C2676","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"947e5398223830d4c80e75386dbd3c8e6dd67f1d","datavalue":{"value":{"entity-type":"item","numeric-id":429585,"id":"Q429585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1702893$B611D606-A2D2-4052-A15E-67FA5DDEC238","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":"Q1702893$C94DE88C-E99E-40E6-BF51-3341D179A8A7","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3ead1def560b38beae02ca12f5c5bf33059d8b8e","datavalue":{"value":{"time":"+2018-03-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1702893$3E15DECF-9BBF-48FB-BC88-703BB67AB02D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b3d92f173516ff164a60d6f6f591f09054092d49","datavalue":{"value":"https://arxiv.org/abs/1502.04464","type":"string"},"datatype":"url"},"type":"statement","id":"Q1702893$CF60D083-8F19-41E3-BD40-505BB80EC90E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1702893$C5AC64E7-3F32-46F7-A424-4DC32CD07449","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1702893$4D68E182-4A3E-4207-9F56-284CB9A18BC9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f2955e4f3fcd4736aac56b174f1974df245d3e82","datavalue":{"value":"6845633","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1702893$241F283E-CCBE-4B50-AA74-3C75D5C7F6BE","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2822825cdea331aa7c0ec2c340c1eb36d62db00b","datavalue":{"value":{"entity-type":"item","numeric-id":17123,"id":"Q17123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1702893$9C43F963-C909-4ACC-AA16-81F5A50CA0F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"45fa147ad24d78ff9111165d21eddec7203c8bfd","datavalue":{"value":{"entity-type":"item","numeric-id":20838,"id":"Q20838"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1702893$B66164B0-D07A-48AF-AB06-A27EB172D5DA","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":"Q1702893$68B17C13-1FDD-4606-AE15-E8C98812BF10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fd1f11f1c714006456b4bd54bab92a11b4a8c134","datavalue":{"value":{"entity-type":"item","numeric-id":40388,"id":"Q40388"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1702893$643AB9ED-2ACD-4536-ACC2-091C0772A337","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":"Q1702893$8A2E8CFC-FF64-4C1F-8158-0DD8430096E1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"62ea436df4522d7967ba1b6144b6afa8a82f3937","datavalue":{"value":"W1912569824","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1702893$B54351C7-B972-4FA0-A7A1-9BBC8DF4467E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"87d3c9e48f94c94d2d69862e627d4883b274b86b","datavalue":{"value":{"entity-type":"item","numeric-id":2280222,"id":"Q2280222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ddb3370c22bdc769f1706e64a8b484ed4ff33ef1","datavalue":{"value":{"amount":"+0.9304112195968628","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":"Q1702893$BF9269AA-3D91-4D6F-BE77-3AE997A0B41A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aff2de331bc83ddf4b0fb5cfb40830bbf057100b","datavalue":{"value":{"entity-type":"item","numeric-id":3303898,"id":"Q3303898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"44f017934a8dc18a8d0007da61537ea8ec7098c1","datavalue":{"value":{"amount":"+0.8255089521408081","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":"Q1702893$0AB2BBAD-3C34-45F7-840A-E43A262BD3E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5a01942a02711b00fe4d9ca41ae8b4ea9eaaf7d6","datavalue":{"value":{"entity-type":"item","numeric-id":6045008,"id":"Q6045008"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b6ef869cd099a527ce7ccd375ff5b3d40f8d81c1","datavalue":{"value":{"amount":"+0.8018832802772522","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":"Q1702893$A4C38B18-9603-4604-8CF3-714A23DFAB7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"42cace2ddf6019b7cd2939e3da583d3a9bc71c2a","datavalue":{"value":{"entity-type":"item","numeric-id":2233503,"id":"Q2233503"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e779ae0561ea0489484c6f00a93172d30a47d6b8","datavalue":{"value":{"amount":"+0.7783523797988892","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":"Q1702893$F792C16E-2B82-4842-A9D5-AF8736D930FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5286bf29d1aaa2124996c5dbc7629f045b4580ef","datavalue":{"value":{"entity-type":"item","numeric-id":2152655,"id":"Q2152655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e12e8b64437e77c4bdc785826390a46fc6de7dfd","datavalue":{"value":{"amount":"+0.7697491645812988","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":"Q1702893$4C1ED0E2-BD3C-43AC-BD4E-33B35CB4610F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Counterexample-guided quantifier instantiation for synthesis in SMT","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Counterexample-guided_quantifier_instantiation_for_synthesis_in_SMT"}}}}}