{"entities":{"Q4930589":{"pageid":6960171,"ns":120,"title":"Item:Q4930589","lastrevid":91659650,"modified":"2026-06-04T23:44:21Z","type":"item","id":"Q4930589","labels":{"en":{"language":"en","value":"Encoding techniques, Craig interpolants and bounded model checking for incomplete designs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5793456"}},"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":"Q4930589$1E597C27-DE63-4AFC-B8EF-7DE298765A60","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6b0ca937af8e941fc6994a5e1c6326a0abf3ae64","datavalue":{"value":{"text":"Encoding Techniques, Craig Interpolants and Bounded Model Checking for Incomplete Designs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4930589$02612967-B491-4907-B675-27E5CAEE7F1C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"cb81efdc3610c54ac603e99c0e7bd7209bed1cf2","datavalue":{"value":"1306.68168","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4930589$54B7AC5A-CA3E-4E8E-A20C-B781D27EB392","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c5a52c11dca3b4d85215ff24dd1429617c440b32","datavalue":{"value":"10.1007/978-3-642-14186-7_17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4930589$3D2E8CEE-5D25-4F8E-9CFB-9799447AED07","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3d732c8553e3ab8d788973b67196e28e36fe8e5f","datavalue":{"value":{"entity-type":"item","numeric-id":1877144,"id":"Q1877144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4930589$F228B902-EBC5-4EC3-8935-2A3770A81F46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8442bf396f27de6e98eec1975d8eb2ba71a58714","datavalue":{"value":{"entity-type":"item","numeric-id":453485,"id":"Q453485"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4930589$F8D5A4CF-8C54-4B0D-A00C-9CD7FB3E64BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e00e442a62e05c062829e5d8e9aedccc1d8d3476","datavalue":{"value":{"entity-type":"item","numeric-id":453486,"id":"Q453486"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4930589$BC990E6D-7B87-4135-9FB9-91D8884FC6B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0db1c1d4758cc84ba91e5181bfa794ba378ebc68","datavalue":{"value":{"entity-type":"item","numeric-id":402124,"id":"Q402124"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4930589$DA1488FB-FED1-44CA-8EBE-805CA994F91F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d1b19733acdd40acbba69ca5d986f1f385209d79","datavalue":{"value":{"entity-type":"item","numeric-id":4930573,"id":"Q4930573"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4930589$C969D917-C999-4285-BE0F-C8B67585F7F6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4858cb14fe2ceb550c09f1dbe5241e082f5548d2","datavalue":{"value":{"time":"+2010-09-29T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4930589$4F3E873A-EDB1-4634-8E8D-82A3BAE53E94","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4930589$5CA0B2DB-BB59-44C7-8EDE-8E20BA7E0CC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c1d2d83da0d870574277144fdd1db9abaae162ec","datavalue":{"value":"03C40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4930589$610B6800-AE5E-4799-94AE-675FD1FF5856","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4930589$3C1404F6-8139-4C45-AB90-FCB51C622CBD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1e903e68a16880f66ed79a0863889f1b2d3c837c","datavalue":{"value":"94C10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4930589$C8224014-8421-40F7-9AA7-8212C81FE9C5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"33411fd691dd0eb71e920770e9794c35de08649d","datavalue":{"value":"5793456","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4930589$773FA96C-D7C7-4F3A-9BA3-6F5BE4C5831C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"82450bed172977afbb20c270b28a2d47d2b23411","datavalue":{"value":"BMC","type":"string"},"datatype":"string"},"type":"statement","id":"Q4930589$8D46ACC3-27EA-4F66-AE62-7F858DC5C91C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"53f5b0b19fe4e4f140c8797819464978596ff472","datavalue":{"value":"blackbox","type":"string"},"datatype":"string"},"type":"statement","id":"Q4930589$92D16B2B-1669-4635-BBC2-7C0511A9E18A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5867ec7b44aefc01672736513dfe6410a0300cd5","datavalue":{"value":"SAT","type":"string"},"datatype":"string"},"type":"statement","id":"Q4930589$C29E03F1-BFF5-4A7D-88D9-920246ABA769","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4dc78b1e4558056e875de92cbf8329d0562afe86","datavalue":{"value":"QBF","type":"string"},"datatype":"string"},"type":"statement","id":"Q4930589$EC4E976D-5A07-4AAA-98EE-E43DB60C3C59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"03f1ce721ffa5b2f36084f57048f17032077e128","datavalue":{"value":"Craig interpolation","type":"string"},"datatype":"string"},"type":"statement","id":"Q4930589$4424E454-5B44-4A38-A043-C90AD2E99D71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"595034c2c7548026a60994257fab840676d5ea6b","datavalue":{"value":"unsat-core","type":"string"},"datatype":"string"},"type":"statement","id":"Q4930589$20B9C45F-657F-46E1-8BA0-9A52D29C1675","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":"Q4930589$0332E55E-BB2D-4720-B8C6-125638A217AF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"9aa3fbea66f1bddfc53587c892baf16e172aab5b","datavalue":{"value":"https://doi.org/10.1007/978-3-642-14186-7_17","type":"string"},"datatype":"url"},"type":"statement","id":"Q4930589$D5974CFD-3DCE-420F-839E-EC82B9769485","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"903e88a3b12832489f52b1f8b9e26a327176567b","datavalue":{"value":"W1495288201","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4930589$9C9FD2A8-BA00-4995-9B3E-E7F56CBA806A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fb253fb55714f511287e3fb7db3bf54cfc2f7066","datavalue":{"value":{"entity-type":"item","numeric-id":5311270,"id":"Q5311270"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3df61996a3235c24f4a54d53a521aa9f0a5ac7ef","datavalue":{"value":{"amount":"+0.7479475140571594","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":"Q4930589$611AF12C-4C49-4001-80A2-F22A656DA90B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d45dd440df75f6c635ba254138a56ee3d488dded","datavalue":{"value":{"entity-type":"item","numeric-id":5900666,"id":"Q5900666"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fcd67dfd1970b36b091d04e561ca0e7433d9ff2e","datavalue":{"value":{"amount":"+0.7286413908004761","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":"Q4930589$4C42B8A3-E219-4B8F-AA18-A6B16340634B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"190233e20cb25d8f3400a4a2388d08bb56869ee6","datavalue":{"value":{"entity-type":"item","numeric-id":5492987,"id":"Q5492987"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bf17d07595c19dcf1657bcd714fe7dc18d4846ce","datavalue":{"value":{"amount":"+0.7244829535484314","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":"Q4930589$961AC6EE-1C96-4D25-8C2A-F7DA69B799A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"518885e28866a0866b78e3ca37da9115ea508c48","datavalue":{"value":{"entity-type":"item","numeric-id":888467,"id":"Q888467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"782479ed594a8222a57273f4ef22a787ad6f7a1b","datavalue":{"value":{"amount":"+0.7178686261177063","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":"Q4930589$84F04878-5FD9-4F34-9BBC-C342905D2154","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0ce1fcb06b0c1223160a39dcef1f6b076a95dd86","datavalue":{"value":{"entity-type":"item","numeric-id":4589096,"id":"Q4589096"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"47491c45b8a1b1fad5b0d003b206501737834750","datavalue":{"value":{"amount":"+0.7166962623596191","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":"Q4930589$073FFC5C-E86E-4E8E-8715-3DF55B9876D8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Encoding techniques, Craig interpolants and bounded model checking for incomplete designs","badges":[]}}}}}