{"entities":{"Q5458341":{"pageid":7487900,"ns":120,"title":"Item:Q5458341","lastrevid":50333843,"modified":"2026-01-13T20:27:15Z","type":"item","id":"Q5458341","labels":{"en":{"language":"en","value":"Quantified Invariant Generation Using an Interpolating Saturation Prover"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5262386"}},"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":"Q5458341$1C330200-20FA-49CD-B416-A8768C7AF197","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fbdd7924511b5521d5b8b0f4978f538366a09253","datavalue":{"value":{"text":"Quantified Invariant Generation Using an Interpolating Saturation Prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5458341$BE23AB03-1F10-442A-98C5-AA51EE7875E5","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"336115de1706a837440b50f693cfa390898fe2b1","datavalue":{"value":"1134.68416","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458341$3A09AD2C-BD6E-4AE4-B089-09603A7F7A06","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9f78e7a1d5917f016425ad316f79cb76b07936e3","datavalue":{"value":"10.1007/978-3-540-78800-3_31","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458341$0C10C9F8-5E39-44E5-9D6D-94AB76A871A1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"57a84b3343ed70002617a9eb1439c18c15bac9ff","datavalue":{"value":{"entity-type":"item","numeric-id":934708,"id":"Q934708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458341$B65BFE69-91F1-4DC0-BB03-BDF88E053C3A","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":"Q5458341$AC2DFF9D-C8A8-4FD1-A319-0CFAE57541EC","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":"Q5458341$9D5360C0-BE0D-4CC4-9E02-7F3F1AA01565","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458341$9B552E9F-85AC-4F98-971A-32E0490F2D19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458341$FD735C54-AD9F-42F6-9CC3-6879DCDAC7CC","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c9da736d2eaa7575cb8c04ea412bc7d2cc0e0172","datavalue":{"value":"5262386","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458341$2D730BE7-3AFC-464A-8B6F-2FEF0EDDF477","rank":"normal"}],"P1463":[{"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":"Q5458341$36CD4B65-5C9B-47C8-9079-14AB220625F5","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":"Q5458341$4713681D-26F3-4D69-AD04-AE3C1DFFD8AB","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2ed3cffb43c2921ad4c526be5b42e94857544ada","datavalue":{"value":"https://doi.org/10.1007/978-3-540-78800-3_31","type":"string"},"datatype":"url"},"type":"statement","id":"Q5458341$668B3884-1772-4588-9FC6-E6846FE3F1E1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0b41485406cd43bb61200be6c802fbb2a881d6d5","datavalue":{"value":"W1517192598","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458341$7ECB4072-9953-44CC-99C9-7B8D6E9BD177","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dfa5b8ee219383bf057660ccaa8422e52df4e875","datavalue":{"value":{"entity-type":"item","numeric-id":2887061,"id":"Q2887061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e00e5fc67e4a16d8c3a57d0b37be05b96adf4cf8","datavalue":{"value":{"amount":"+0.7809466123580933","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":"Q5458341$9B7E2322-2F22-4608-8054-C5608153D3ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"192babe1f332f85d504aff10a4562aaa3e265788","datavalue":{"value":{"entity-type":"item","numeric-id":5308386,"id":"Q5308386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c6e5dbffcf80fc85fb77629233d51dee1e9b636b","datavalue":{"value":{"amount":"+0.7795388698577881","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":"Q5458341$CF708F80-86D6-46E2-BC54-99815B46B3F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e412e6216b54f0d01b161d965adaae87ffed390b","datavalue":{"value":{"entity-type":"item","numeric-id":2575736,"id":"Q2575736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"014c5feac20d9abaa5b0fad9e1e8254a250e9b20","datavalue":{"value":{"amount":"+0.7792564630508423","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":"Q5458341$BCA5DB13-B6B5-49B2-BD07-ED38EE4AB57D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1755c681f2850b9c2be50d8a3f34fae490a03b10","datavalue":{"value":{"entity-type":"item","numeric-id":479820,"id":"Q479820"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dbfed314b4844de3832e6cf54248d409b438e4d8","datavalue":{"value":{"amount":"+0.7741559147834778","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":"Q5458341$21B33F5E-C504-4B93-9BD9-0EB630765195","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"72ac296eef685af3714af18edb241e087213d64e","datavalue":{"value":{"entity-type":"item","numeric-id":5890659,"id":"Q5890659"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eb17fff2847ab232dd20e5095bfa56fec90da664","datavalue":{"value":{"amount":"+0.7734177708625793","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":"Q5458341$E40CFF1F-C406-4439-9BBA-3F48D7115866","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5458341","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5458341"}}}}}