{"entities":{"Q2864382":{"pageid":2875102,"ns":120,"title":"Item:Q2864382","lastrevid":79490312,"modified":"2026-05-06T14:01:54Z","type":"item","id":"Q2864382","labels":{"en":{"language":"en","value":"Interpolant learning and reuse in SAT-based model checking"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6236392"}},"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":"Q2864382$99D95912-750C-49AF-B622-600B15EB6E52","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"df355a50f180a9d78256d493a78aa0bc8be9c2f5","datavalue":{"value":"1277.68140","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864382$592C48D8-9627-4A0C-828D-255D542DB82D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3478ec308a15597e43cb648673c843463f4d3028","datavalue":{"value":{"entity-type":"item","numeric-id":163528,"id":"Q163528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864382$10132A79-A2AE-460C-95CB-F0E0FF7D3619","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"deb6cb3450bd256fc635dc32234471403070c2b7","datavalue":{"value":{"time":"+2013-12-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2864382$B9F1A9BB-9DAA-4014-B74D-739123D53ACF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864382$0BF875F3-62D0-4951-B99D-B26C1A3BD0D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864382$792E4EC2-04F7-409A-B6B8-AC89D5A54910","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9cc0ed6fdb2981c4d51a79ab0a42aec8ceb78a1f","datavalue":{"value":"6236392","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864382$766849FD-D054-4891-81D6-CE1F07C230EB","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3978d2f31bc86b19c4025fe772ec1974bbd09669","datavalue":{"value":"Boolean satisfiability","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864382$A03A7E47-2D4A-4831-953D-BC6EAA299259","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e6ab41959fd9494b5548d09c762ca90a9336e1c7","datavalue":{"value":"bounded model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864382$943DF07B-1A72-4B89-B24E-5CCC4EDA83F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fa2c0f78c04a92c7553072540610ce03525a9448","datavalue":{"value":"interpolants","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864382$E49971C5-1DF1-442F-ACEF-9BB40DE8D9AA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"41df06f4fe4133fafd7ede4eda94dd022be9bb8e","datavalue":{"value":{"entity-type":"item","numeric-id":1430295,"id":"Q1430295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864382$D7368759-52F7-47B3-9CB4-FEABF33609ED","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b029c35ffabe60b7d29584a6d40b4cb278ba542d","datavalue":{"value":{"entity-type":"item","numeric-id":18983,"id":"Q18983"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864382$FF5AA17F-44A2-470D-9B66-868983B9A75C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8449db7d9aaa28101ba7b0de8e98d9c446365070","datavalue":{"value":{"entity-type":"item","numeric-id":13332,"id":"Q13332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864382$5EA9D66B-3D5C-4B95-A1EC-62BF6F921FB3","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":"Q2864382$328A6A21-92A4-4E27-AA5C-77242D50BF57","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"535f8f3c90d41583bfa5e7b4f55765c042d93a1f","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2006.12.021","type":"string"},"datatype":"url"},"type":"statement","id":"Q2864382$D74D23A9-A50A-4C04-B237-B3123B3DED45","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1c7b0c20d06bcb021d0931b18cb146238841dd8d","datavalue":{"value":"W2129952473","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864382$D4DACBEC-6006-4184-82D9-312F6547A691","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"140707a542a9d45a6f78619413d8c06c89d7576f","datavalue":{"value":{"entity-type":"item","numeric-id":2729082,"id":"Q2729082"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864382$3023C1A5-0099-4916-BE3C-5139BC331620","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb19e18c12ddea2b553dcb695cb9473546265295","datavalue":{"value":{"entity-type":"item","numeric-id":4427894,"id":"Q4427894"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864382$F58A131D-35C0-4232-9026-2D4DB1BC5D57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a179078c9a9f8b24e5164f170dbd1be09ede2650","datavalue":{"value":{"entity-type":"item","numeric-id":4551177,"id":"Q4551177"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864382$8170065C-D693-47DA-8865-2582C13933BE","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":"Q2864382$46CB5F47-EAE0-425A-B7C9-CBCE871800D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62cff4d07ffcb71b5bb9f399ad2347b51931f095","datavalue":{"value":{"entity-type":"item","numeric-id":5621961,"id":"Q5621961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864382$D21D777C-AA68-4E13-B51E-D6333847358B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c0e6b90c16ae5fa1eac19212a306cb84ffec72b","datavalue":{"value":{"entity-type":"item","numeric-id":5613969,"id":"Q5613969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864382$9C85015E-4414-4C93-B444-62DBE61F3AE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22485e2e7f5d751287059d6c89f8749b6a408a20","datavalue":{"value":{"entity-type":"item","numeric-id":5325885,"id":"Q5325885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864382$33E920B1-C50C-4C7B-9F72-39CFF31D872E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d421342230c67a224b42e44ea336b06445d9587a","datavalue":{"value":{"entity-type":"item","numeric-id":2845506,"id":"Q2845506"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864382$807B7695-D9CB-4080-8C95-99950CEB3601","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e4de8e02463aa9adeead8bdc6d0fc6c098b1202","datavalue":{"value":{"entity-type":"item","numeric-id":4417922,"id":"Q4417922"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864382$582B549D-4ECF-4F75-BBF2-29626F91F81E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3348c4f23a620a7654545e9e3737b9f755ba6069","datavalue":{"value":{"entity-type":"item","numeric-id":2643301,"id":"Q2643301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864382$CABAB60D-637D-4AD7-A5D5-79A01E2B623C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62dd1223d29569eec68058706eac7eb8d1b02072","datavalue":{"value":{"entity-type":"item","numeric-id":5493247,"id":"Q5493247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864382$844885E5-6679-4C26-AD3C-39B0EDFF9BD4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cee1f5c4e596769f20c3e18240de0776d1bbf0f7","datavalue":{"value":{"entity-type":"item","numeric-id":4804900,"id":"Q4804900"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864382$3889BD72-8EFE-4B4E-819A-C04E913C3849","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":"Q2864382$739298DE-1C8E-4460-9AD9-A54798A3955D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c7ee42bcb5651ff1d6441d36735f61656172044f","datavalue":{"value":{"entity-type":"item","numeric-id":4417909,"id":"Q4417909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864382$0DC29479-0051-46D2-9A20-E291726F089C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"008723b33cb14bbda59226503d753d137dc6f8ef","datavalue":{"value":{"entity-type":"item","numeric-id":1098330,"id":"Q1098330"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864382$DCAF94BD-BF28-4C96-A9F2-2E06E5B56ED3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"40f34823cac176489a74f3e54ebb7fe9577d93ab","datavalue":{"value":{"entity-type":"item","numeric-id":4372917,"id":"Q4372917"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864382$501D5A28-E52C-439C-B6BE-8B13BA5418C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a0b3ec2ebad61e0cf6b1df8ac8c200c146db0252","datavalue":{"value":{"entity-type":"item","numeric-id":2754108,"id":"Q2754108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864382$6406457D-2AD8-454E-BF74-DF755695DE41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e98bea2faf0f1e7139247049b725eb54de257627","datavalue":{"value":{"entity-type":"item","numeric-id":5593816,"id":"Q5593816"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864382$5496F206-A532-44EC-9A48-4A318FFF2D5B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d39f1986116fa81e2fc95288d41f1cf2f3870aeb","datavalue":{"value":"10.1016/J.ENTCS.2006.12.021","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864382$288EDB18-5E39-4D00-9ACB-C0449F12A3A2","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fb5e44f140dab8a31109329358c415520b0ce897","datavalue":{"value":{"entity-type":"item","numeric-id":5166692,"id":"Q5166692"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2426a21d4cf18235a95aa03060f35c093cd7f9f8","datavalue":{"value":{"amount":"+0.8899244","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":"Q2864382$74AA0101-B9A8-437F-8B79-937400EC4D1C","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":"0e96c68a4428eba0216c9dad57689b28a8ed8df1","datavalue":{"value":{"amount":"+0.88513875","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":"Q2864382$0053FE56-DB82-429C-899D-5536EBE96864","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e2f42da8edbca079b6a499d2bad177c9e5e69247","datavalue":{"value":{"entity-type":"item","numeric-id":6102162,"id":"Q6102162"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e1c8b42ba6f912b9c6aeb65a930e68bf83963fe2","datavalue":{"value":{"amount":"+0.87441295","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":"Q2864382$43FD97CA-AC98-4120-9661-39640C26BFD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3a1cc29d937cf08a8209142db26e225a778d772b","datavalue":{"value":{"entity-type":"item","numeric-id":6041187,"id":"Q6041187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5bab86e6d11ed4bf1c49f507eec7c10e0a96cab8","datavalue":{"value":{"amount":"+0.86907965","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":"Q2864382$90E3E7E4-60F3-4E78-9CE6-630F99C0A941","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d6f754bdf912eb9b6aed20d0b7a354284c47bd11","datavalue":{"value":{"entity-type":"item","numeric-id":5458340,"id":"Q5458340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d982e3e250513cb2bf74ad3d372755b92e35eb7e","datavalue":{"value":{"amount":"+0.8672154","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":"Q2864382$81233B7D-8079-44BA-BC87-1ECBCDAFCD34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6082005cb838151ec2f536065030af8f23f991cc","datavalue":{"value":{"entity-type":"item","numeric-id":5452599,"id":"Q5452599"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ef42c1eb6ee2dd6f92e50a91884b41e1f02858d4","datavalue":{"value":{"amount":"+0.86258125","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":"Q2864382$D31AE9E4-80AE-4535-A38A-E4ED00EE5493","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b843e9a65e168ffb5723cc45f81c92fab43633a6","datavalue":{"value":{"entity-type":"item","numeric-id":1647700,"id":"Q1647700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3eb5b81736c546bba32a5cae10ec1882d7a26f47","datavalue":{"value":{"amount":"+0.8584012","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":"Q2864382$EB5E6EF3-9D7A-4460-9A37-4BA0D4E654D6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1f2e54aedbe89251a79533fb242e404c342fdece","datavalue":{"value":{"text":"Interpolant learning and reuse in SAT-based model checking","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2864382$C84074E5-023B-46A0-8AB7-9B34EB23276D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Interpolant learning and reuse in SAT-based model checking","badges":[]}}}}}