{"entities":{"Q2907311":{"pageid":2918036,"ns":120,"title":"Item:Q2907311","lastrevid":51548438,"modified":"2026-01-18T17:56:57Z","type":"item","id":"Q2907311","labels":{"en":{"language":"en","value":"Challenges and experiences in managing large-scale proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6079487"}},"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":"Q2907311$F4110732-1D9B-4377-9922-63707F340510","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6275547dae8475060e88e84f97270481b905eb16","datavalue":{"value":{"text":"Challenges and Experiences in Managing Large-Scale Proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2907311$C23F2530-17FF-4915-A553-9ECF42CC52BF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4bcaa58454618d55c0553e0557802d1b89d03066","datavalue":{"value":"1359.68264","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2907311$FB8A0500-23DE-40B9-9EDD-FBC5EAA27FD2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"365201b528fa311f970cf11c942b62ae5e0b15e1","datavalue":{"value":"10.1007/978-3-642-31374-5_3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2907311$BFDBA4C6-09C0-42EC-BB0C-7AB5BD7EF0BB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1933122bc86d2597add2b8555d2985101b991054","datavalue":{"value":{"entity-type":"item","numeric-id":287370,"id":"Q287370"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2907311$4259F5B0-5BD2-4084-84D2-7D98F7950FE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e5b560f397084fe8f43e4a8b2d11676ab9b22052","datavalue":{"value":{"entity-type":"item","numeric-id":736845,"id":"Q736845"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2907311$E6822F5E-C882-4CE9-84F3-3C6E1C23EF31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"008a47245ae11ee2f12e0bd284b000b43ab772af","datavalue":{"value":{"entity-type":"item","numeric-id":736847,"id":"Q736847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2907311$79475918-BDE0-4AE7-AE68-BD28FF310D75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f12962e861bcd5806794148f68880772868b69fa","datavalue":{"value":{"entity-type":"item","numeric-id":2907310,"id":"Q2907310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2907311$4F6E6E11-D199-43AA-AB32-EF0D2A534A9A","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":"Q2907311$37293B19-9CCE-44ED-A569-55ABF683676A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f0d54a7a192189275358732a85216bf3ce89224c","datavalue":{"value":{"time":"+2012-09-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2907311$A7B9BA9E-9605-4665-97B7-8A4A8F1E4FBB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2907311$1C0A1593-0FCE-4E4A-AF08-41DDA089CCBF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"22944d3c2dd14a89b7a3dfc30f53e0d5ca850f23","datavalue":{"value":"6079487","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2907311$3F6B3483-6DA0-4635-B12A-F06C94D561EB","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"64e3ec159ae7a6a853255afc23a8b641a213bce4","datavalue":{"value":"large-scale proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q2907311$CA2D8226-2C4B-4CCB-A566-7259A62EFE32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42f0513e500ea6cb630e73925875c7d53ca8d8e1","datavalue":{"value":"Isabelle/HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q2907311$0B893457-8C91-4D2D-9E58-2A4EC5B3D326","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2907311$14F6875F-4F59-401A-9652-3A0A30065A4D","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19c3232540dc15c9350e8393498317de25361cb2","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2907311$EAAA9747-69D5-46A1-ABBE-84FCCCCED991","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9b0860d94af5fdff4b5635709ae334aacdf07ca1","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2907311$A9855796-DACC-4C5F-9C74-BE13189130AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"25db55153babd7076d594d911b639e78d62b451a","datavalue":{"value":{"entity-type":"item","numeric-id":20369,"id":"Q20369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2907311$E0C2C00A-87AB-455D-B188-35C27B48CB20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e338912f65cbd77347bbd512933e55736ef58bd1","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2907311$1568DE3F-4D10-4B58-8CD1-0CCE7E43AF3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2907311$17D28372-25BB-4CBD-94FC-B6FC41E9840C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2907311$F4D67D50-7D55-49B0-8666-99EFB85DF6FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19db008058ce3a679389c190541b4b00e350555f","datavalue":{"value":{"entity-type":"item","numeric-id":27113,"id":"Q27113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2907311$18DEFE1C-6C28-40F3-97CC-362A65E32DE9","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":"Q2907311$EC9C9933-4A49-4DFF-9C20-CDAC7ABED83E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4ab14e03014ee372799fe167eddac9213420f919","datavalue":{"value":"https://doi.org/10.1007/978-3-642-31374-5_3","type":"string"},"datatype":"url"},"type":"statement","id":"Q2907311$9E68AAAA-9C48-4EB9-BD0E-8722BF4E8157","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"cf41745487914e89ee0c028b1fc0aef2468197da","datavalue":{"value":"W1537943690","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2907311$F1118D08-7C6A-424D-B2FB-EB330EE89848","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"27834f8881d79d504650b55693f4830b894523f6","datavalue":{"value":{"entity-type":"item","numeric-id":4530805,"id":"Q4530805"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c3712a44a85172b80cfc56f014095d99ee8372f9","datavalue":{"value":{"amount":"+0.7105075120925903","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":"Q2907311$9B885A08-DC31-4340-A4EB-558751B4E877","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"55e08d4c1b4a36ec698bdc3aa8756e9e8896d4ff","datavalue":{"value":{"entity-type":"item","numeric-id":4787230,"id":"Q4787230"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"30fe099919edfe1101264738794988ff334f8300","datavalue":{"value":{"amount":"+0.6949766874313354","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":"Q2907311$BC24FED9-2177-41A8-9235-1D3EBA14F2A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b343ddeb7b8723940bff14faa8c0877850c55d01","datavalue":{"value":{"entity-type":"item","numeric-id":2879265,"id":"Q2879265"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b5549f0be6a2591eea3445ae5d1026e4a98154e3","datavalue":{"value":{"amount":"+0.6710491180419922","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":"Q2907311$A7A9182D-CDAA-48A5-B536-CB38C3D36DA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"018780f278d91b1e97c8f1940276e2350ff28205","datavalue":{"value":{"entity-type":"item","numeric-id":6039756,"id":"Q6039756"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"05d84f46723b5290b5148b0ce1be0803ec4be973","datavalue":{"value":{"amount":"+0.6708999872207642","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":"Q2907311$184C5704-BACE-4443-B72B-F9BCC9731B5A","rank":"normal"},{"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":"7e671e7f450f6bfdac19aee6881cd6c4255c090e","datavalue":{"value":{"amount":"+0.6706864833831787","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":"Q2907311$D9EBE206-C4B8-4CE0-8B83-5C6FC70BE203","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2907311","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2907311"}}}}}