{"entities":{"Q5458340":{"pageid":7487899,"ns":120,"title":"Item:Q5458340","lastrevid":50333840,"modified":"2026-01-13T20:27:14Z","type":"item","id":"Q5458340","labels":{"en":{"language":"en","value":"Efficient Interpolant Generation in Satisfiability Modulo Theories"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5262385"}},"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":"Q5458340$7A8ADBC9-20A6-4A3B-B234-2BCD910E141A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5bf72ccc88f32499afefd7c0900ff04eda440d4b","datavalue":{"value":{"text":"Efficient Interpolant Generation in Satisfiability Modulo Theories","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5458340$40180243-2B24-4EDF-A44E-814B72242FC7","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6dec2af7ce0a72c649e2498b02a3c28d35731cf7","datavalue":{"value":"1134.68402","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458340$CB031D41-5E20-47C7-BFFE-0B80CBBE4EDA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f5d5d1efb938849c697a15013f4bdcff23267710","datavalue":{"value":"10.1007/978-3-540-78800-3_30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458340$C3285BE0-C57F-4DCB-ABA9-0D5D8BEA1E3E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"387e6ac60ed3a0144bb303179c23c53493d401d0","datavalue":{"value":{"entity-type":"item","numeric-id":329418,"id":"Q329418"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$CACCF4DB-9C13-4816-9F28-2DAECD5A90AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e97e7d65eece04188cb1a1dff66ddc09c38fbea4","datavalue":{"value":{"entity-type":"item","numeric-id":479835,"id":"Q479835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$36CCEE13-98FE-4F60-BBB1-74960361053D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4fd5a076641129df5baba24779caed9dec893447","datavalue":{"value":{"entity-type":"item","numeric-id":511776,"id":"Q511776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$44E50356-83F5-4054-8358-0AC0A6B25EBB","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"0caef843b05c7cfb5667c1a8106613cbf61a6d23","datavalue":{"value":{"entity-type":"item","numeric-id":2894263,"id":"Q2894263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$FF00DEA6-25E2-4A2E-A37D-E85DCAB1E846","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"de5306c1211a7dcd78b6214088eb3e5b7092fd16","datavalue":{"value":{"time":"+2008-04-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5458340$F8866489-0721-4789-B8E0-46777BB2D414","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458340$64A7CF32-A736-418B-B4FF-403AD2E42506","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458340$C491105C-0F04-458E-9605-EE7849B460A6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4b25c4713dc298b4ef8cb0f5e0e0fc4de3df3172","datavalue":{"value":"5262385","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458340$70BCFF84-3E50-4DC4-9135-0321C6BEEE96","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6bd3e17f5c8106c552732e5d9395b841a42716c0","datavalue":{"value":{"entity-type":"item","numeric-id":18897,"id":"Q18897"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$1EBBDA46-9FB1-4AC9-85E6-CB539B0F4124","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6c46d83f8225e8e4d789b6fc74144d78a1809470","datavalue":{"value":{"entity-type":"item","numeric-id":24792,"id":"Q24792"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$57338EC5-95D2-4920-8A3A-E708C68DC450","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":"Q5458340$01A010DB-6149-4802-8D0F-536227EDF176","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d7e622d41cd39be076be5b9723fab86ca04cb712","datavalue":{"value":"https://doi.org/10.1007/978-3-540-78800-3_30","type":"string"},"datatype":"url"},"type":"statement","id":"Q5458340$23910833-FF5D-4F29-A173-5A1956E597B7","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9c2f6091a66634bd22886db274fc94e95c247757","datavalue":{"value":"W1499948164","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458340$FA5B5418-0B21-4C2F-BD4C-E974CBBD1FED","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"bb04d80310fb506ec6d9da913bbeb7c34a35b99a","datavalue":{"value":"Q62041289","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458340$D7D0A516-8844-4D68-9FB6-EB0CCDE5568F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca50b56de23777ce618ce7b9747f11712b65365d","datavalue":{"value":{"entity-type":"item","numeric-id":2849590,"id":"Q2849590"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$D4AFC8D2-3092-4CB0-A1A5-8A2A45FA531D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93883db00833e89e855c8e92c4e962692b3eeca8","datavalue":{"value":{"entity-type":"item","numeric-id":4422082,"id":"Q4422082"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$D7F47F60-FB6F-41BB-98D9-62A5A076DFB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2caba9f0c64300d40671e9474a40a9e638624b84","datavalue":{"value":{"entity-type":"item","numeric-id":5387827,"id":"Q5387827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$3001FAB3-1E6B-48F2-84AC-6E01165975ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5ffd063b19f75595f78df5a07ec83544c6e288d","datavalue":{"value":{"entity-type":"item","numeric-id":862395,"id":"Q862395"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$A9CE59ED-245F-42E1-91CC-ED01180AB8A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"38b0f81481964ce2c3959f44994546ec67aa5a63","datavalue":{"value":{"entity-type":"item","numeric-id":2432765,"id":"Q2432765"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$3EB4DD2E-14C0-49B3-AE94-7300E6C7EB85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cc40c812d63ac65a43f7097e08e541074138fd0b","datavalue":{"value":{"entity-type":"item","numeric-id":5387917,"id":"Q5387917"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$4266CD6C-ED7A-4B5A-B22A-456D350E1CA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da0010e327ddd368956022cbe52c271ac71c9d3b","datavalue":{"value":{"entity-type":"item","numeric-id":5458340,"id":"Q5458340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$08D2D3CA-CD59-4347-89DE-468FF90900CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f1c9b30d63dba402510d5838237495966fbe464","datavalue":{"value":{"entity-type":"item","numeric-id":5756581,"id":"Q5756581"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$6CEB2B60-B103-4C18-9CFB-49887313BDC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4e94238a6a5ddf3dd15f03313efac1f027d9611","datavalue":{"value":{"entity-type":"item","numeric-id":3452263,"id":"Q3452263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$9AC19A45-D9C2-4ED5-849C-03DC11231A6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"af62bfd2162dabdadb1d68f1499174dc7482fad7","datavalue":{"value":{"entity-type":"item","numeric-id":5716597,"id":"Q5716597"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$7A79183E-EA1C-4B3C-8B16-03147D2B0017","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce3bb918603ae315ee0224631b7326b49acf86c5","datavalue":{"value":{"entity-type":"item","numeric-id":5899073,"id":"Q5899073"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$CB0175AC-9DE6-4A51-845A-FECCCE6F66BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9d0dd7bb6db6a4c0ce328175c5c1c2e0bc50527","datavalue":{"value":{"entity-type":"item","numeric-id":5429322,"id":"Q5429322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$63A72CB7-625F-4937-8349-BBFFD06E5893","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9bf74af701b8385747cfada5ecd2ea6d2b1e199","datavalue":{"value":{"entity-type":"item","numeric-id":5899061,"id":"Q5899061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$50C7483A-868E-4425-87C7-8BD997C0F7C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c550ccefa8c33e8450539a2f7f48c280b0c29631","datavalue":{"value":{"entity-type":"item","numeric-id":2864382,"id":"Q2864382"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$0BC10AFC-0D87-4F1B-9197-6D5FD1207352","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":"Q5458340$40FF5C22-B708-463F-B41D-3C07735A2B1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ef9c0e492b02772fdee855678eeaaecef66c13a","datavalue":{"value":{"entity-type":"item","numeric-id":2575736,"id":"Q2575736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$87C81FCA-9AE1-4A36-AA8D-EE9E57259EB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e2d9d5673d377c95422809e446c2052b58cca8ec","datavalue":{"value":{"entity-type":"item","numeric-id":5756749,"id":"Q5756749"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$D1231E1F-814B-452E-A2DD-F43EED3F6059","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce7b2dd2863358cf2a528999ec6b006fdf400b99","datavalue":{"value":{"entity-type":"item","numeric-id":3899468,"id":"Q3899468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$831CD70B-4BD4-45BB-BD7F-B27E0071832B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a09716697edb234ce77c2288fe827cd22e3a8915","datavalue":{"value":{"entity-type":"item","numeric-id":876046,"id":"Q876046"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$16E51989-BDD9-4C61-B693-4D46761E84DC","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":"Q5458340$E3C0D115-1310-429C-B5F3-99037378A144","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ed0c5a805e2d83d2fc67d0e9100dbfc3999c3a60","datavalue":{"value":{"entity-type":"item","numeric-id":5452619,"id":"Q5452619"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$50EF0E9A-57F5-47F2-8153-49036C756F13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7b1ef4c8566673a8a5c94d00ea3fc5ee04078d8e","datavalue":{"value":{"entity-type":"item","numeric-id":3506045,"id":"Q3506045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$C66AE61D-8E81-4E85-9AED-04A800202C8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a85f7dd9005efbbf5a53b34d69354b11263cd606","datavalue":{"value":{"entity-type":"item","numeric-id":5946779,"id":"Q5946779"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$65B68A9E-0BF7-4C0A-B33F-CC54F00B3DFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b7903ffd8f9b852f272a22a95cb583ad2910295a","datavalue":{"value":{"entity-type":"item","numeric-id":5394624,"id":"Q5394624"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458340$5AF1CD07-4B8B-4BEE-B2AA-89E9EC58E27C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"89dbb15b892cff2f017253eeff9ee21c526689af","datavalue":{"value":{"entity-type":"item","numeric-id":2946624,"id":"Q2946624"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d604060184c6acd8cdb2b46ab0cd75cafd80fd68","datavalue":{"value":{"amount":"+0.9144887328147888","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":"Q5458340$621C0A74-3386-4808-98D6-9421364A2D43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0d0acf781d81a37d8deb3e20167f9211fb090938","datavalue":{"value":{"entity-type":"item","numeric-id":5892495,"id":"Q5892495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b9e77ac093ba060e837a7d479f5ca0bf28192857","datavalue":{"value":{"amount":"+0.8845938444137573","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":"Q5458340$133940BF-F473-4986-BED3-2753A6523157","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"13004038faffc696fbd1f83fa37d6804792ecd3b","datavalue":{"value":{"entity-type":"item","numeric-id":5891705,"id":"Q5891705"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"76b014fcae77c9fb2e8a7b18a6ae2878e1fd59a5","datavalue":{"value":{"amount":"+0.8803223967552185","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":"Q5458340$C72F3E1E-89A8-4D13-9518-50370D53751A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9230814f4bdae60126ac2fd4bca89d8927256e1b","datavalue":{"value":{"entity-type":"item","numeric-id":5191101,"id":"Q5191101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c95ef95d4c25553503a87bc07b96747593707c8b","datavalue":{"value":{"amount":"+0.8347131013870239","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":"Q5458340$26E88B51-CF1F-428B-9F86-AFD92A92936E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"983f12d49d1082c01b8f635af6ed51965a406a38","datavalue":{"value":{"entity-type":"item","numeric-id":3460545,"id":"Q3460545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d9c081b6ccf30fb602066d870b059fea51e5f46d","datavalue":{"value":{"amount":"+0.8277142643928528","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":"Q5458340$67510AF1-E3DB-4DED-B042-A6AE1FACD144","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5458340","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5458340"}}}}}