{"entities":{"Q3523178":{"pageid":5553082,"ns":120,"title":"Item:Q3523178","lastrevid":50441513,"modified":"2026-01-14T01:43:45Z","type":"item","id":"Q3523178","labels":{"en":{"language":"en","value":"Source-Level Proof Reconstruction for Interactive Theorem Proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5318947"}},"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":"Q3523178$A4E419D9-40C0-4B54-B08D-20C8BC407C74","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a87819140be92b74da81b48799c3a05c3efb5f08","datavalue":{"value":{"text":"Source-Level Proof Reconstruction for Interactive Theorem Proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3523178$9EECE9EC-4185-44AE-9A9A-8E825F3AE9FE","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"362bffd0925d12897e1296b5d937772c013bd9cd","datavalue":{"value":"1144.68364","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3523178$0C3783FF-BE79-4D9C-8D09-EB9244D2FE4C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0d9d801458386d560c2b9e7282273e8deaa7d871","datavalue":{"value":"10.1007/978-3-540-74591-4_18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3523178$E9B2D65D-B615-4B48-B11A-482A794A433E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"dc335a6bc0a2bb1dfda61d59af8f1a38bd938fb6","datavalue":{"value":{"entity-type":"item","numeric-id":207985,"id":"Q207985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3523178$FDDCE475-60FF-4A4C-B9BF-BC2BD0F3A141","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cb5dfbdfa6d8a2070a67ff948fb8abd387eda36e","datavalue":{"value":{"entity-type":"item","numeric-id":352969,"id":"Q352969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3523178$D9779DBE-39CD-4F33-9477-319A58CB99EC","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3523178$7A01E8CD-85E0-4237-BD77-96E33FF55E6B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"20b7f535510e218ce28c7540c7cdc4660c15d850","datavalue":{"value":{"time":"+2008-09-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3523178$E87B9DB0-3DF9-4D15-8D11-0808A1547537","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3523178$517797E8-AA3A-48D4-BAD3-A4EE778BCB37","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"749237328776aced254815b40fc287a609977c01","datavalue":{"value":"5318947","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3523178$C4EE47F8-3C90-4382-A407-3F46CF8B3C14","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3523178$6B6F4068-8C0A-4285-8244-760308F15367","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"43f7c4ee5068daf82f8bffbb0f7510a5f16faf63","datavalue":{"value":{"entity-type":"item","numeric-id":16615,"id":"Q16615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3523178$BB2EAB44-3099-48E6-9EF7-7C2741F9A3F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"af3b5ddb4818ec81bb9bea3bab4852742bff1bd5","datavalue":{"value":{"entity-type":"item","numeric-id":22101,"id":"Q22101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3523178$4B284642-C5BE-4441-B32E-0E126F78A841","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1017108dce3983431546a14c274f65bc4aaae70b","datavalue":{"value":{"entity-type":"item","numeric-id":22154,"id":"Q22154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3523178$14C06DB3-20BD-48A1-96C5-2CFE03F346FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b443b776731e3bc75eb79b752e7ef8c4cee2d97a","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3523178$7F2CEEB2-D21C-498E-8C74-1053555A2702","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3523178$E8907B2D-D742-4E4D-A9EF-39E9195B0C5C","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":"Q3523178$FBA11DF4-11EC-4D99-8932-5A9C15CE34CC","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b97238671f4911b07e80e1c741c34240263814ac","datavalue":{"value":"https://doi.org/10.1007/978-3-540-74591-4_18","type":"string"},"datatype":"url"},"type":"statement","id":"Q3523178$934E6098-8FC6-4E31-9BEA-3FAE1AF7A615","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d914b871c04d8b485805cbff0fd3ec0ed1b7fde6","datavalue":{"value":"W1524804222","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3523178$FA53414E-5A1D-46E3-B091-AA66156748F0","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8db65f4a30f1bfae13dbc2dde40a4f8521358003","datavalue":{"value":{"entity-type":"item","numeric-id":2432769,"id":"Q2432769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b63124f6c21fc723233c7999030f77c8337a4c89","datavalue":{"value":{"amount":"+0.7867249250411987","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":"Q3523178$C32715C0-DA51-4793-9E16-00D3F16347F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5f94645fe7f1525963701159b1c6851e22f8eef0","datavalue":{"value":{"entity-type":"item","numeric-id":287340,"id":"Q287340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"308814ab8bd17db2ba24b828b1a288b72ab335df","datavalue":{"value":{"amount":"+0.7608590126037598","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":"Q3523178$C825BD4E-7063-4421-9971-ABCD3192AA4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"da0657b25dcc4d374ea3510625bc156a46f79a85","datavalue":{"value":{"entity-type":"item","numeric-id":2964467,"id":"Q2964467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ea818821a447469152cac42ffbd8eeddea7d79a0","datavalue":{"value":{"amount":"+0.7569076418876648","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":"Q3523178$DA18DDF3-8110-43B2-92A5-8A230D2A1CA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"83ead96eb0dad59b33308a29c10c00c5949abf9c","datavalue":{"value":{"entity-type":"item","numeric-id":2723415,"id":"Q2723415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f82a4076d6296870ac78d845ff2d09528d761f46","datavalue":{"value":{"amount":"+0.7490589022636414","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":"Q3523178$919CF31E-0F15-43A3-AE63-0DC50AEE1E17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d31ac5b611e1dc394bc6dbb9071cf4d1998a3862","datavalue":{"value":{"entity-type":"item","numeric-id":4524769,"id":"Q4524769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c92260ec852b6acaf19049c71cd4441748aa5fb3","datavalue":{"value":{"amount":"+0.7490583062171936","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":"Q3523178$48F15B41-085F-4317-9E90-91A434A0103F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3523178","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3523178"}}}}}