{"entities":{"Q2234081":{"pageid":2244824,"ns":120,"title":"Item:Q2234081","lastrevid":71633994,"modified":"2026-04-13T23:32:48Z","type":"item","id":"Q2234081","labels":{"en":{"language":"en","value":"Syntax-guided synthesis for lemma generation in hardware model checking"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7410645"}},"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":"Q2234081$EF3C1F0C-AED0-4EA0-A5B1-FE1796511070","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fe8a38c22488dfa649e4ae11a630466463e20b1d","datavalue":{"value":{"text":"Syntax-guided synthesis for lemma generation in hardware model checking","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2234081$0D682F87-4AC4-4693-B740-48C5EE66DDD1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"474eefd4ef0a5e5273f09dc3a56b599ef3daa6be","datavalue":{"value":"1472.68096","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2234081$69E45459-CEF8-4E95-A972-F556921FFB45","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"99a71b08be7e2e4732176e19dd5eca9e8cc802e8","datavalue":{"value":"10.1007/978-3-030-67067-2_15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2234081$A1AF0915-7E70-425C-B48D-A23C930B048D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e294939c34f6df60e834188d62266fff995ba51e","datavalue":{"value":{"entity-type":"item","numeric-id":784128,"id":"Q784128"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2234081$F40462A3-ADC4-4FD6-82D9-121390A75009","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"267769ee025773c3257f441a0558f5f2a60f51b9","datavalue":{"value":{"entity-type":"item","numeric-id":432145,"id":"Q432145"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2234081$EF59ABF7-0689-4393-B6CD-C778394FB643","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ad84ce20d471d4eb62ee7ab9f8f8819cbe6311af","datavalue":{"value":{"entity-type":"item","numeric-id":265699,"id":"Q265699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2234081$9B67D8D3-64F8-43F2-A2B0-46FF07189335","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":"Q2234081$3521703F-345B-445A-9969-A3F2D8A47B57","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2234081$CACFE0FC-7522-4A21-B784-1B50865402C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"cd80e9ade304e6b9b43fd50d0c3436276c3c217e","datavalue":{"value":"68M07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2234081$CC0A860A-BE31-4B01-BB76-0D0CE0DEADB4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c55ee2d5f334fd4a7d69a1ecc9e2ffcc52cfe89c","datavalue":{"value":"7410645","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2234081$BE7161E0-6BC0-4AB3-8E5F-EF104981C04D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3840a64590fd40658a14d6184275aac454c0e76e","datavalue":{"value":"hardware model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q2234081$A710CEEA-5381-4255-A1F2-E8DAD87F20B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"72ef84f322f22afac00de2b767e90b99f09cfb83","datavalue":{"value":"syntax-guided synthesis (SyGuS)","type":"string"},"datatype":"string"},"type":"statement","id":"Q2234081$DE5416F3-4E33-4430-A4A7-79035B74D7FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2d9b3c3f716fa4bae84586bb8cf0e7ce4470f70b","datavalue":{"value":"bit-vector theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2234081$904282D6-6EDE-4584-B23D-8F74CC22962E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"20e8523755c629936b223c108cd9b934e50817c8","datavalue":{"value":"lemma generation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2234081$C824389A-3A9E-4C31-8F1E-58CEB537A4CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7dc9e4229d50e9a879864eb10e061a933b1fbe59","datavalue":{"value":"CHC solver","type":"string"},"datatype":"string"},"type":"statement","id":"Q2234081$EBF03896-1318-437E-96A0-5F57565F4BA5","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":"Q2234081$E994954F-5BDB-4039-9513-29E63C6757AE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d8a8cae17966738b7bc235d3f3999d8a274f8010","datavalue":{"value":"https://doi.org/10.1007/978-3-030-67067-2_15","type":"string"},"datatype":"url"},"type":"statement","id":"Q2234081$DA509D58-D205-4C8A-A655-5DDE03C3C237","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"fa28ef0456602a9295f6de906a1c89766673ac78","datavalue":{"value":"W3120833016","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2234081$BA4AA07E-64C9-401E-A70B-ACA922A6BE84","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"dbd5e9b7224b44a5be727c6870f16a737b8c3625","datavalue":{"value":{"entity-type":"item","numeric-id":2769592,"id":"Q2769592"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2234081$F427605E-BD17-480D-8C00-64BD834B4EF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"48c2c388a22640ac9d5b19d2053fe4b933139852","datavalue":{"value":{"entity-type":"item","numeric-id":5172647,"id":"Q5172647"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2234081$DF304545-3421-43B1-850C-7F1A925D33C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb2ada01f2a5df2219780857a93a43f3585326f1","datavalue":{"value":{"entity-type":"item","numeric-id":6091330,"id":"Q6091330"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2234081$8093BDD9-8360-42B5-A21A-BDF51DE6FD7F","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":"Q2234081$E8CC0107-A34B-4BF5-9E21-ECECDD468457","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ef993e1a6f9e1affb5ec0a35f6683de283af104b","datavalue":{"value":{"entity-type":"item","numeric-id":2441772,"id":"Q2441772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2234081$8CAF3F52-668A-4F0A-A51E-D8CE700F5C3F","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":"Q2234081$197E9A33-B210-4C65-BEB6-B84266F13CA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b026130fb14abb6ec25af9a49779c945ecc8f0fd","datavalue":{"value":{"entity-type":"item","numeric-id":3452508,"id":"Q3452508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2234081$9177FDAD-D717-4B09-94A5-36DF16F8790E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8092a4684ef7778dba1ddad2618a794c87412cd6","datavalue":{"value":{"entity-type":"item","numeric-id":5227061,"id":"Q5227061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2234081$CA3013E9-D65C-4D6E-AC12-7927A9611859","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dca7b9a18761ceedb11c92011194ff5c5e5af826","datavalue":{"value":{"entity-type":"item","numeric-id":4633554,"id":"Q4633554"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2234081$FDB5DFD5-0955-4FEA-8F7B-EA00481E1C9F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7c4cf2cc00850270a28614888dcd0fd49d3c89ac","datavalue":{"value":{"entity-type":"item","numeric-id":2225478,"id":"Q2225478"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2234081$00B98B75-10E0-42BF-9034-534B75914F33","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":"Q2234081$6E34CF94-8A3B-4546-88B5-2490377F4558","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c36c36a33f99dd120f8ee638e971c8b19f681cb1","datavalue":{"value":{"entity-type":"item","numeric-id":2226726,"id":"Q2226726"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2234081$DED39867-51EB-4322-896F-DDEF551EC648","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eaff131682deb6ad1bffecaae47bca13d452055a","datavalue":{"value":{"entity-type":"item","numeric-id":300418,"id":"Q300418"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2234081$63BF2A9D-0FDD-4D8B-852C-CA87494CC211","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"91a574c680e43eb60952b94dd4450a5aded3487c","datavalue":{"value":{"entity-type":"item","numeric-id":5311270,"id":"Q5311270"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2234081$B61FF753-2B49-4918-BD6F-BB862B548DA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"348369ca3fccbe91226809a75cbf31afd7f3186d","datavalue":{"value":{"entity-type":"item","numeric-id":5900666,"id":"Q5900666"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2234081$7ADB8E4B-A62C-491B-917E-39B318D8E79B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a0ac8008fc7a5a5734156abe6133cadbaa63c0ab","datavalue":{"value":{"entity-type":"item","numeric-id":6194583,"id":"Q6194583"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2234081$B589CFD6-B107-419C-8E67-36897A67EF98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0b669ff01773fb618375d501feb0b3033d40d4ce","datavalue":{"value":{"entity-type":"item","numeric-id":2226732,"id":"Q2226732"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2234081$0CC9350C-DFF8-4F69-89ED-218129788855","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"48ce097ac54a7e4155b36a538c9575e607272270","datavalue":{"value":{"entity-type":"item","numeric-id":784131,"id":"Q784131"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2234081$AEB3B8FE-8F3F-4AD5-99D4-A678D2591565","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"81fb1657427495232c5ae2608a0e6d15ca998a89","datavalue":{"value":{"entity-type":"item","numeric-id":1702893,"id":"Q1702893"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9fb82e2d7e93f2862b79e188d5861ab9d1b083b9","datavalue":{"value":{"amount":"+0.6892355680465698","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":"Q2234081$0DB37ABC-BC9E-44B9-A5FB-43A42B1C24AF","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":"6b08a8b06f2ea0c5a8d276b33c1015db26f2b093","datavalue":{"value":{"amount":"+0.6883240938186646","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":"Q2234081$000674B4-ED69-4FA4-8836-676292435CF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e8ce1097c6167bdccb5f2d7cbdc69f8c9f518514","datavalue":{"value":{"entity-type":"item","numeric-id":1039855,"id":"Q1039855"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c8e9df91fce15fd67e6d7411e8f21ffb8f64afb6","datavalue":{"value":{"amount":"+0.684738039970398","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":"Q2234081$87F8ED12-12BF-40DD-A5E1-E3AEAE9ED071","rank":"normal"},{"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":"d0b9028a50f2692077d9bfce42d241c2ecdd35bb","datavalue":{"value":{"amount":"+0.6794894933700562","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":"Q2234081$CE75A603-1912-453D-91F7-DEEC841CEAD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7402074e23113d3349cf30046c1ec1c19b1f6812","datavalue":{"value":{"entity-type":"item","numeric-id":2938057,"id":"Q2938057"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"82aae255adfc1e3e0fab7797d0f710f0fa91ba1a","datavalue":{"value":{"amount":"+0.6786332130432129","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":"Q2234081$4CF0AB50-BF85-4E79-9B05-457B9F04F285","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Syntax-guided synthesis for lemma generation in hardware model checking","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Syntax-guided_synthesis_for_lemma_generation_in_hardware_model_checking"}}}}}