{"entities":{"Q3460068":{"pageid":5239468,"ns":120,"title":"Item:Q3460068","lastrevid":58184241,"modified":"2026-04-04T03:45:39Z","type":"item","id":"Q3460068","labels":{"en":{"language":"en","value":"Sharing HOL4 and HOL Light proof knowledge"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6528794"}},"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":"Q3460068$F2CC76D4-9B8E-4A8A-9745-1E205EAB3AFD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e947ad981983524d953ef37aceabd0ef9ffe3003","datavalue":{"value":{"text":"Sharing HOL4 and HOL Light Proof Knowledge","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3460068$229D260F-07BD-42E0-BF25-0510D0E3A153","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3cf44cdaefbdded2ebd7b62cd68315de619550f2","datavalue":{"value":"1471.68309","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3460068$62AAE301-B0FC-4B41-AEC1-42FE80C06765","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9ac8b5c15933f892a60fb654f866212f17d2c773","datavalue":{"value":"10.1007/978-3-662-48899-7_26","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3460068$08A3C896-40B7-4DD2-9756-49B6360273AB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c280ac10e768ccaa378c9121429e161719c83e06","datavalue":{"value":{"entity-type":"item","numeric-id":1640641,"id":"Q1640641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3460068$D077FF85-366A-4EA3-A82C-988A9AD6865E","rank":"normal"},{"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":"Q3460068$A5AADBC0-8979-4119-8520-992B2DE22EEC","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"23864e2be568bb8a6a4b0526f5a5216348320070","datavalue":{"value":{"entity-type":"item","numeric-id":2870110,"id":"Q2870110"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3460068$117A7A75-A1AF-42F9-87CE-51398C31AE2D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f91432dc3d3ba35c1a5312422600047e5b632480","datavalue":{"value":{"time":"+2016-01-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3460068$6F2917E6-82A5-4E50-BDEF-BAE75FA61AF5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7c76618b76d37a7d0ecdfbfe92f64d5c59cc6c6a","datavalue":{"value":"https://arxiv.org/abs/1509.03527","type":"string"},"datatype":"url"},"type":"statement","id":"Q3460068$27B58740-CB63-4560-9721-1A7A0E96CCD2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3460068$DAB5D80D-E44B-4C67-8A75-794D5A3C1DC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3460068$E95F62EF-7B63-486A-A7E5-FEB1D377F453","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4c276f6bcfe480cdd0a7a976933d6fd851c1b746","datavalue":{"value":"68V30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3460068$25B95554-D1FF-42FD-9BA1-B16FF378AEBD","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e5d5dd661b4a43829de8e349f0ab22b9ed4948ff","datavalue":{"value":"6528794","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3460068$3BAEB6C3-72B4-4648-95F8-FDFE7EB04040","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3460068$2A67DD35-A709-4C5D-83B7-93F4A7C26CE1","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":"Q3460068$8522C076-2D0C-4CFD-A143-1B52314479AB","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":"Q3460068$06183FA2-F48D-41E5-A558-521D3FEBA4DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"23f1d4970d4f2ba01b8146500b5c1a10ed17d235","datavalue":{"value":{"entity-type":"item","numeric-id":23493,"id":"Q23493"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3460068$B6BFAA21-C9E9-4E45-9216-9A3A79E992CC","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":"Q3460068$642F16EA-3616-453F-B38D-54D7315C65C4","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"01d09442d19cfb2d184f93d7affc1ced587dee66","datavalue":{"value":"W2229278275","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3460068$41F45DCD-8F67-4335-B3AF-2C58E6477389","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"c9618f503e79ee2faeabf5223d787af0991c6ee3","datavalue":{"value":"Q108482162","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3460068$F8870BB2-7648-44A7-9496-EE2159397FC2","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3e6e726c1ccf3d48bbd9191c4571af0a1046a6a6","datavalue":{"value":{"entity-type":"item","numeric-id":485842,"id":"Q485842"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a792062be5dd2686802bee85c65e192ef0f9b553","datavalue":{"value":{"amount":"+0.7887324094772339","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":"Q3460068$6B57FE07-10C7-49BC-B994-E67CBB2EAD61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"80a02b86f5e7c12a000ea62837c3061ae5ebea26","datavalue":{"value":{"entity-type":"item","numeric-id":4645730,"id":"Q4645730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"58561039debf443d188ce4405aebba9e2da55c09","datavalue":{"value":{"amount":"+0.7708450555801392","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":"Q3460068$A7B6827D-775C-472C-8E78-ABE93D16BA21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"62eb5673352ddfd5c999328fdcfb0b637fbd9630","datavalue":{"value":{"entity-type":"item","numeric-id":2351415,"id":"Q2351415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5549f0bb3f6d5ed4bd42db29a7be102e3de4a834","datavalue":{"value":{"amount":"+0.7668042182922363","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":"Q3460068$55B6B8DA-CEE8-4E1F-A5E6-E7DB3ECD1C75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"85400645ae2fb59fc9cccff35e42a877cc96a4b5","datavalue":{"value":{"entity-type":"item","numeric-id":2843009,"id":"Q2843009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8c5a03d360f567ed028a86166c886266923b48a0","datavalue":{"value":{"amount":"+0.7532488703727722","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":"Q3460068$0B4F0510-2013-4F09-B1BF-624A6420F098","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6e2ce9d05c86c088573e2213f25dbf60f15f642e","datavalue":{"value":{"entity-type":"item","numeric-id":4524774,"id":"Q4524774"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3dbd084a3cea710cbdca4808fe61bcb146c82045","datavalue":{"value":{"amount":"+0.7521466016769409","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":"Q3460068$62998106-960A-44DF-9BF5-7D193ADBE0B2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3460068","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3460068"}}}}}