{"entities":{"Q2907308":{"pageid":2918033,"ns":120,"title":"Item:Q2907308","lastrevid":58061958,"modified":"2026-04-03T15:58:20Z","type":"item","id":"Q2907308","labels":{"en":{"language":"en","value":"Dependencies in formal mathematics: applications and extraction for Coq and Mizar"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6079485"}},"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":"Q2907308$E198729D-4FB6-4F22-98AA-2F2CE49FDAD8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2bfdae9ddbf47b6ba86dfd6dd26c0539690e8e0c","datavalue":{"value":{"text":"Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2907308$215BE5E4-9D97-49EC-9303-73E2F2E4DD7D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d0a4c8192f3be351acf80c4d3e7e3b460bd7bb61","datavalue":{"value":"1335.68221","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2907308$0E6355E8-85B8-4777-AE5D-E154FF93DD95","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a9013620d507a7218067bcceda106f66b30d49fc","datavalue":{"value":"10.1007/978-3-642-31374-5_1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2907308$9F78AA02-AE7A-4E5C-B217-EBFDBEFA68BB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"263b3b42f52ae45efd16753ae3b4c5178f9c0385","datavalue":{"value":{"entity-type":"item","numeric-id":456971,"id":"Q456971"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2907308$AFC80C47-EB13-42F5-A88B-AF247204D581","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4695f91e84f51db7c19d41787e60821e6561f914","datavalue":{"value":{"entity-type":"item","numeric-id":2907307,"id":"Q2907307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2907308$759B1B34-A884-4ADF-9D23-0B485BA7C664","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"dc204e2e78d924e815f2b640ec35c8c2356ad41f","datavalue":{"value":{"entity-type":"item","numeric-id":286786,"id":"Q286786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2907308$C8E868CE-C36F-478E-9916-58C91D7F2C46","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":"Q2907308$75E243E2-732F-4F34-AB71-D7803A3091EB","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":"Q2907308$D25C2C96-C2E3-42AF-AA7D-6D6BB9DD7919","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4554fec2c7c81827b1618256d338d16a5f183934","datavalue":{"value":"https://arxiv.org/abs/1109.3687","type":"string"},"datatype":"url"},"type":"statement","id":"Q2907308$342C2B87-9CED-47F0-8DB3-7275FB1A63B3","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2907308$76972272-3E6A-422B-8414-89CE1B192E5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"0c6e71133293256880be082f6af9aa793c57d433","datavalue":{"value":"68T30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2907308$464A2352-32C9-4D07-90CE-5AE8ED2DAF29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a50ad10d859c37581a66df0bd2c759d3d47ad6a4","datavalue":{"value":"68U35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2907308$A0D3874A-1157-4450-865D-444D7FE64264","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3f9b10ff871e6ae45144ec7cbbded6e33f51b480","datavalue":{"value":"6079485","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2907308$6B336D21-E30E-49C3-AD75-93B4407553D7","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7cccd35b34888307d4ad7b137783609eb5c56b79","datavalue":{"value":{"entity-type":"item","numeric-id":16825,"id":"Q16825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2907308$8D4FDA3F-FCFF-4988-98FF-B3802920BFD4","rank":"normal"},{"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":"Q2907308$3571DFC9-769D-4DDF-8350-088A4F520813","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":"Q2907308$CF682897-79AD-4180-A886-CFADD2BE142F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9c2ac6c1c15bd263207487c53115a7cc6abe2547","datavalue":{"value":{"entity-type":"item","numeric-id":19033,"id":"Q19033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2907308$24B63369-930C-403B-9578-511BC00CE380","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":"Q2907308$C8E46F06-4CDE-4C11-B8FD-BAB3326E398E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c6ce2714964cda88de666b0e44e4053b91e0b406","datavalue":{"value":"W3103563805","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2907308$2A5046D4-004F-4047-AD10-44C1029A6DF3","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3db6d199add8d33f3d913b30a13b7b56d2fd080f","datavalue":{"value":{"entity-type":"item","numeric-id":5200124,"id":"Q5200124"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"56f34be45a60b6d6007d6b20da1e274024140995","datavalue":{"value":{"amount":"+0.7761932015419006","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":"Q2907308$4C7D7C55-F7C5-4772-AE9A-CB4226E4F4BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fe515488258d2db9b5d4cf4365cd7b9479c86c63","datavalue":{"value":{"entity-type":"item","numeric-id":2364689,"id":"Q2364689"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4e73b3b23136516fa8a9b372fb9d0563fa15390e","datavalue":{"value":{"amount":"+0.7268816828727722","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":"Q2907308$097390D9-F727-436B-9760-75DFCD5EEFB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3791ebade564b3137ef470985cf98685e0f9b0b8","datavalue":{"value":{"entity-type":"item","numeric-id":4413879,"id":"Q4413879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"abcc0ddf5f3f80bcbbc3400e4ada86fc3b777f36","datavalue":{"value":{"amount":"+0.7223819494247437","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":"Q2907308$249C5C13-5D70-4D28-BCFA-3976133181BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a5225a69bdcfcfe29a5db8c4b18a78ef5cb47fe6","datavalue":{"value":{"entity-type":"item","numeric-id":4413892,"id":"Q4413892"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4288dc35bb6ba285e85e8ffe7d78494523157b48","datavalue":{"value":{"amount":"+0.7054659128189087","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":"Q2907308$9E39ED3B-02A4-40D8-9E47-064DFA3E8192","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d4f05aee4b3664e67f1ee18f25367507e60b89a0","datavalue":{"value":{"entity-type":"item","numeric-id":5313080,"id":"Q5313080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f583e5d6e546c56c963ef2f43711cdb11a86189b","datavalue":{"value":{"amount":"+0.705007791519165","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":"Q2907308$1E31DBA9-F9AA-45BE-BEA0-97FA927918EC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2907308","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2907308"}}}}}