{"entities":{"Q2867935":{"pageid":2878655,"ns":120,"title":"Item:Q2867935","lastrevid":51894950,"modified":"2026-01-20T12:05:23Z","type":"item","id":"Q2867935","labels":{"en":{"language":"en","value":"Web interfaces for proof assistants"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6241758"}},"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":"Q2867935$E561D5C1-5B97-497F-9774-F22FB5F16C66","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"973debd73885e0909bc6a013c96064cfe7158165","datavalue":{"value":"1278.68266","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2867935$0BE8C5F9-508D-46BD-B320-DFF4842D4419","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6ad6a046b48bbe4ab777309f1d5c19b5fc7dfbda","datavalue":{"value":{"entity-type":"item","numeric-id":286799,"id":"Q286799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867935$BCD54178-6FF2-4CFD-9F5D-CB16A9027632","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3478ec308a15597e43cb648673c843463f4d3028","datavalue":{"value":{"entity-type":"item","numeric-id":163528,"id":"Q163528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867935$F21DACD5-58D4-43D0-9CBB-464B60FE67CB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"910ae69968b0b824ffb07e2bd5cc35370f9e2a13","datavalue":{"value":{"time":"+2013-12-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2867935$68FE2AB8-A87A-4AF8-802B-F499E2C744C1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2867935$69475B7D-95F8-459E-BCD6-2462392ECF59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a50ad10d859c37581a66df0bd2c759d3d47ad6a4","datavalue":{"value":"68U35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2867935$91CF883E-5085-4AC8-A3A3-B51EA00E6417","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c52a0436823df1e65d57d7f23683c3a265a45ac5","datavalue":{"value":"6241758","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2867935$27097C64-21B8-44A2-9558-E8C40C4376C4","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6a78675f0dcb3af511ac1d4dfa61901e828bcb8","datavalue":{"value":"proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q2867935$382AE280-748E-4EA0-BB1C-66B65749C054","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6f53d67912f1afa2c169e3f8f3e5f1b73f9d88b7","datavalue":{"value":"interface","type":"string"},"datatype":"string"},"type":"statement","id":"Q2867935$1CDE2945-725F-4423-A42D-8FBBFED81B76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fe906f4d109549c7340062fc696143290c97a3c4","datavalue":{"value":"web","type":"string"},"datatype":"string"},"type":"statement","id":"Q2867935$686DA46E-8116-4807-AB65-7B633B900162","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q2867935$253B0F61-A652-42ED-A84B-1937D36DD22B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7da515b2478ded20d9414f6fab0a4407db77940b","datavalue":{"value":"asynchronous DOM modification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2867935$9780FC57-5D61-452C-BD27-4818187FCB91","rank":"normal"}],"P1463":[{"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":"Q2867935$4B568BB9-8A4E-4E11-A88F-EB642A93DD57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e74e65aea50b572ed5cc320d9d0d7a2d70ec494a","datavalue":{"value":{"entity-type":"item","numeric-id":21666,"id":"Q21666"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867935$2C3AAF6F-1833-423A-8A62-C350EC69AFF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"535ea9c4e9344ec2d2bf7c52debe0dc9b157ac7f","datavalue":{"value":{"entity-type":"item","numeric-id":21948,"id":"Q21948"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867935$972F1CDC-B83C-4AA9-A892-3AF31250972F","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":"Q2867935$588078B7-D033-4E59-983A-0DC13BFC33A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9aeef25d5839625565921d83cf1c652bf6f2fbf6","datavalue":{"value":{"entity-type":"item","numeric-id":17052,"id":"Q17052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867935$E03E9784-3EA9-4E31-80CD-5CBF6D85C08C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7bb1c7eafdbb853d5fe04051d89b8463fa8b943a","datavalue":{"value":{"entity-type":"item","numeric-id":18827,"id":"Q18827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867935$32B87825-3A6C-4CE8-AD84-1ADD77402C30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6eebe30b9df25d8c347930b235e09f446ddc2fb1","datavalue":{"value":{"entity-type":"item","numeric-id":44157,"id":"Q44157"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867935$E1D2F4F5-10B0-4CB7-AEFA-8B919E50D601","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"322cfa9d250a6a53032394dc0d9f662b03cdb062","datavalue":{"value":{"entity-type":"item","numeric-id":19193,"id":"Q19193"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867935$470E67BC-8238-43A8-9B29-3ADCB04461B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c3aa95a2ec2e1aefe26078e8381cd9d370c279f9","datavalue":{"value":{"entity-type":"item","numeric-id":21663,"id":"Q21663"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867935$EDD31920-DBE4-4488-A047-FCC141D099E3","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":"Q2867935$AE2BB696-B734-4982-A65B-CBE227C35959","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"9234c8ce929cb154e7f0ee116827cd8be04ca0eb","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2006.09.021","type":"string"},"datatype":"url"},"type":"statement","id":"Q2867935$CE33E314-2C27-4D15-90E7-7055160859B8","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f5b54426def283725cb7f8371be06d99ab9ce616","datavalue":{"value":"W2169030566","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2867935$5FA87326-A6F0-4564-BB65-25DC82BAE02C","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"227fc9bce9cf15c389748b111a74b48d46473f02","datavalue":{"value":"Q108482197","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2867935$E93489CF-8213-4F60-8D65-2300ABDDCC6F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"34babec465921f60dcf35356976f5e24742b5ce1","datavalue":{"value":{"entity-type":"item","numeric-id":5898170,"id":"Q5898170"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867935$7A294561-BAFF-4BF5-B158-CE9CBFDCBB71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f652ed67f57587bded49ef3bafa72146cdb69090","datavalue":{"value":{"entity-type":"item","numeric-id":4790651,"id":"Q4790651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867935$A4A92C4B-4279-4484-956E-1E8520249296","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1196f5e17dff99bc1a9d16ec3c58ef966832597d","datavalue":{"value":{"entity-type":"item","numeric-id":2729065,"id":"Q2729065"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867935$C49FD639-05D5-430C-AC1A-6CC5AB3F2EEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a8e3517581f053bd397311cfe8d27c9b34620e8a","datavalue":{"value":{"entity-type":"item","numeric-id":5234706,"id":"Q5234706"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867935$ED90B740-7DBA-4A1F-ABD5-68CC9E76A242","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e7df3906eae3c2b887cc910e28b2339b9830fc52","datavalue":{"value":{"entity-type":"item","numeric-id":5313080,"id":"Q5313080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867935$EF26347A-9CE8-440F-BEE2-67001F33223E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e7da6c6cc89a0a581bea44c94961c1a898809f4f","datavalue":{"value":{"entity-type":"item","numeric-id":4471938,"id":"Q4471938"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867935$E49C8D0A-3643-4593-9DD9-D30BACF1A242","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2cfd356224155dbd75db29249481baba3510e2a8","datavalue":{"value":{"entity-type":"item","numeric-id":5394302,"id":"Q5394302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867935$D0B6AC0D-F91D-4399-AC75-D3E38603D00B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e77f4bfe2eff062e3e9eb2c9dd8bd3187397271","datavalue":{"value":{"entity-type":"item","numeric-id":1810908,"id":"Q1810908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867935$A104529D-FB85-4758-A021-B831AC1B24F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867935$72BF9FC6-F00F-44DC-B0B5-56F13F1F2337","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4bd19c035a67c1f829baf3c1c19367bed411ba8a","datavalue":{"value":"10.1016/J.ENTCS.2006.09.021","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2867935$8429BE3B-6EE9-4BDD-97BE-AACCAE4D1497","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ddfa6ab6c3cc220c06575232cc4cb6fbdc8e33cc","datavalue":{"value":{"text":"Web interfaces for proof assistants","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2867935$7F449FF0-1E86-4BFF-882A-EECC45D388F7","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bc188bfb4ad5c58a3146fd1cfb32723c348e1eb1","datavalue":{"value":{"entity-type":"item","numeric-id":2843032,"id":"Q2843032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c26fbe023ab93c8cf92060bedef7ddceee3ff2a5","datavalue":{"value":{"amount":"+0.7956355214118958","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":"Q2867935$6A0C1959-B06F-475B-8F6F-A93363D5690D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d66339c795d505f780406e18e20e0f95f8bd017d","datavalue":{"value":{"entity-type":"item","numeric-id":2729065,"id":"Q2729065"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"82c3970704d293a5dc2265cd3c29194b79dec8d4","datavalue":{"value":{"amount":"+0.7675501704216003","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":"Q2867935$82438038-6EAD-411E-B0BF-2795872E995D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0836461b86e5f3f9b2683c3a2c12fce3a6959131","datavalue":{"value":{"entity-type":"item","numeric-id":4664918,"id":"Q4664918"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bb8d615979ef737c935a345b8dd6de0f31889a3c","datavalue":{"value":{"amount":"+0.7597090601921082","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":"Q2867935$E1DAAFB8-0E22-452D-A622-E5E67B7776C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bb049dc19118c2e13b11c57ad63c65e40f939e98","datavalue":{"value":{"entity-type":"item","numeric-id":2879270,"id":"Q2879270"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"785151dfbe07cb47e1b87df9ab624032cd5f0848","datavalue":{"value":{"amount":"+0.7381571531295776","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":"Q2867935$CA425C0F-203E-40F7-9FD9-D9D0A4B99389","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"21ecfb31ea6a40a0d2ae59130ec9f6f04cd0d466","datavalue":{"value":{"entity-type":"item","numeric-id":3582730,"id":"Q3582730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ea3b7fcd1fed79da1c57dd84563e6e25be3284a9","datavalue":{"value":{"amount":"+0.7297974228858948","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":"Q2867935$A341941D-0FED-4787-A229-00AC4868ACC3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2867935","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2867935"}}}}}