{"entities":{"Q6159381":{"pageid":13294214,"ns":120,"title":"Item:Q6159381","lastrevid":55452874,"modified":"2026-02-17T16:42:30Z","type":"item","id":"Q6159381","labels":{"en":{"language":"en","value":"Re-imagining the Isabelle archive of formal proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7691297"}},"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":"Q6159381$A4974C24-CC34-4804-AB01-A090C31BC4E0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"aed74ccc9ef3a0811922a4dc5a3e9c60e97d8ea6","datavalue":{"value":{"text":"Re-imagining the Isabelle archive of formal proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6159381$AA5A48A5-F7D7-4812-B426-0D4DEF16EC6E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6ecab1a4ed93cf5aa1522d5bd7497a63463a178e","datavalue":{"value":"10.1007/978-3-031-16681-5_11","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6159381$B1D7FC3D-16A2-4CE3-BD71-E52AA2F2A23C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6d89fe09fb5d8ca189524272f99107099ec23663","datavalue":{"value":{"entity-type":"item","numeric-id":6159379,"id":"Q6159379"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159381$1E5275EC-BB07-4A6D-85D8-679CD3F6FF20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8f64101566eab5cea5671c31f8e640732e15e1e5","datavalue":{"value":{"entity-type":"item","numeric-id":6118823,"id":"Q6118823"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159381$67AD27D5-D626-49FD-92CC-81845EEB5A23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"61ca170cb9a2e20d78d15fd03c4d9346438465a0","datavalue":{"value":{"entity-type":"item","numeric-id":6159380,"id":"Q6159380"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159381$9BBD4481-360C-4B19-ABEC-71A413767195","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8d78e8b1fd2bada0896418639974db329feb4fe3","datavalue":{"value":{"entity-type":"item","numeric-id":2102945,"id":"Q2102945"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159381$54204C47-40ED-4DD5-B765-39DBE279278D","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":"Q6159381$2677F626-9B1C-419F-9018-6FF41C983C9E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4fa95a2618f91e175d2e6cdf4f6ce4782d828b01","datavalue":{"value":{"time":"+2023-06-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":"Q6159381$7CA6218B-9814-436A-9A77-75EA17C69F4B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"51b7800ccceb407b4c9aa81c10252a3a04dbfebf","datavalue":{"value":"68Vxx","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6159381$48505EAC-7485-46D1-8FDA-D6D64A7E1B83","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"be2ef599b32154c07123ef62c376ccb3ca5d0f37","datavalue":{"value":"7691297","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6159381$CBBF6615-550D-403B-98A4-8958F7DC2946","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7eefb2b1f5e1ddd95f5db204b23cfb4c53d0151","datavalue":{"value":"Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q6159381$D31A08B6-9981-4D60-80EE-8F0B1B4A86E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3ff6db9d16a0ec84f38f8d643901e77bf8b73f45","datavalue":{"value":"archive of formal proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q6159381$37B27BEB-0D78-49C6-95E0-FD10CDADEDCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3dd12981ba79112c8b0b36387f28037a89a463da","datavalue":{"value":"user interface","type":"string"},"datatype":"string"},"type":"statement","id":"Q6159381$F5EE3375-ECB6-488B-9FB4-D7B30F11C58F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"65dcca7367d0f531cd31cecc1a0bed4d7013bafb","datavalue":{"value":"user experience","type":"string"},"datatype":"string"},"type":"statement","id":"Q6159381$D31B91FE-5386-4968-9296-DDBFA3A83D3F","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":"Q6159381$648DCD7A-C100-41DF-AC7E-4C40D4338869","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"4c11c9facaa68035dfd36664b0cfddf618a17c36","datavalue":{"value":"Q114700496","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6159381$91D3EFAE-A727-48F1-9D5C-187BA55E8088","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e87403798c0acb2077feb1a48ae189765245391b","datavalue":{"value":"https://doi.org/10.1007/978-3-031-16681-5_11","type":"string"},"datatype":"url"},"type":"statement","id":"Q6159381$100A0BFE-A4B2-4AFE-AD9F-C1ACE2C3DA7C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"05a52c7264aacc3edea2dba1c4549f6668297864","datavalue":{"value":"W4296050232","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6159381$FC2CBAB0-D423-43F0-81E6-2CE7983DBFBB","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"73bc73e3351b113a1680b6365fb1851ae1d25213","datavalue":{"value":{"entity-type":"item","numeric-id":3453102,"id":"Q3453102"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159381$9145FE9A-34DD-436B-BCAD-9AB089AC683C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e0a521a247c004a14f53f38577ade217c87172ce","datavalue":{"value":{"entity-type":"item","numeric-id":6159378,"id":"Q6159378"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159381$6B71E0D1-5025-41AC-9068-DEA2D354731D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8ccce3a3de5790e22d8d97b965a5abb2eb6a5522","datavalue":{"value":{"entity-type":"item","numeric-id":3453102,"id":"Q3453102"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c127106680575e61ff3db6d35d7caa0e84f3b553","datavalue":{"value":{"amount":"+0.7519192099571228","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":"Q6159381$40076E1E-CFA4-4984-820E-722E48BDF19F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f3b5071d30c3a27e1864a05e8395b498be0cb4a4","datavalue":{"value":{"entity-type":"item","numeric-id":6159377,"id":"Q6159377"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dada3c43592d2d7e0cdefa85e7fdb067c34caa71","datavalue":{"value":{"amount":"+0.7034722566604614","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":"Q6159381$7DDF8706-9935-4829-B00C-6E58F27C5B82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a0cc07b681385ffb864e3e24cf69f53f7eb1978e","datavalue":{"value":{"entity-type":"item","numeric-id":4933332,"id":"Q4933332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f383b360e7e63e4cebcb48296a48fa41b19b534d","datavalue":{"value":{"amount":"+0.6681823134422302","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":"Q6159381$36DB7C7F-621A-418C-AE6B-F112698E0A1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"df287ba4711af7eb66eb6c4530853de65788cc26","datavalue":{"value":{"entity-type":"item","numeric-id":2287890,"id":"Q2287890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"573042dfc6aab76ab3c2780fa027afbd649e460f","datavalue":{"value":{"amount":"+0.6576864719390869","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":"Q6159381$D7DC6398-14B6-46CB-A6B8-962370EDC5CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fc2522fe32f92b0689c3d64c38929bc388d26805","datavalue":{"value":{"entity-type":"item","numeric-id":6635513,"id":"Q6635513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d5946dd6127fa57d86ed7c71bacd1f0c8f92145f","datavalue":{"value":{"amount":"+0.6424594521522522","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":"Q6159381$B4A7F0A7-262F-4BFA-89D1-4B0E0A5E9737","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6159381","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6159381"}}}}}