{"entities":{"Q4928443":{"pageid":6958025,"ns":120,"title":"Item:Q4928443","lastrevid":51744725,"modified":"2026-01-19T19:37:25Z","type":"item","id":"Q4928443","labels":{"en":{"language":"en","value":"PRocH: proof reconstruction for HOL Light"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6176214"}},"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":"Q4928443$A83DE207-5D46-4119-AA6B-FE87FFB0E2E6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b37d96a4b40b376a092bad42d771b3a9e7be26c9","datavalue":{"value":{"text":"PRocH: Proof Reconstruction for HOL Light","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4928443$1FBE1DAD-D79F-4829-956A-E69C726954D5","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"55caca6b1f183d3cf5951e9099167c9046a148ce","datavalue":{"value":"1381.68271","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4928443$21E971B4-3C91-4191-AEB0-A72ED807FB01","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ce41aa0573f760f67e933669ba3284deef466711","datavalue":{"value":"10.1007/978-3-642-38574-2_18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4928443$B84EA3A2-B032-4AA7-A417-645611581544","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":"Q4928443$AFB500EF-72D0-420F-A6C8-6E494676E1E4","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":"Q4928443$4182F03C-F011-499C-BEA6-A9D85338C0CA","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"feba868a8cb9ecfadec66d8e8a91d447de952529","datavalue":{"value":{"entity-type":"item","numeric-id":4928424,"id":"Q4928424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4928443$DD9F5BEB-A561-4029-A80F-11FC173E1CE2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b84d2a34981f1c1a0d0fb543ea5aabc14a21194b","datavalue":{"value":{"time":"+2013-06-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4928443$537DC875-7F59-4EBC-B503-2DCA41A783E3","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4928443$3AD7432D-A746-430C-825C-81A15501E05D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f99cf54383ee9a60e458ba2774eadd8d383c28f6","datavalue":{"value":"6176214","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4928443$9EAB47B5-D975-4F12-B304-5272AF763BF3","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"19012bbeb297a7b2535aac32ca0d3230a5a6465c","datavalue":{"value":"Q108482180","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4928443$8870E921-23E8-4120-A9BD-4D180AB186FC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"18639e33f43106ad1f03f2034efb665fd424d29b","datavalue":{"value":{"entity-type":"item","numeric-id":22242,"id":"Q22242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4928443$BEC1F9A7-FA12-4425-A9C0-85DF1949661B","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"233bd03fc74bc4c01e6f828569e5eb13f94bb747","datavalue":{"value":{"entity-type":"item","numeric-id":22242,"id":"Q22242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4928443$B9E508E1-0395-4457-8A69-812C017B1E81","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":"Q4928443$E2FE6464-F9CA-4C0E-A0E6-4FEB3A97F43D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"43f7c4ee5068daf82f8bffbb0f7510a5f16faf63","datavalue":{"value":{"entity-type":"item","numeric-id":16615,"id":"Q16615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4928443$42E91DD8-4EE3-4E24-AFB6-FA4C7C58EA88","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":"Q4928443$0B6728C1-3E48-4BC7-ADBA-1BDD0915DDD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"66eb045e037081b6f6e8499f9fef44d8fbb7e0b0","datavalue":{"value":{"entity-type":"item","numeric-id":22240,"id":"Q22240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4928443$5B862027-D4DB-4810-B8C7-557D19F16D9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4928443$77086427-6CA0-413D-92BD-91D29D6BE59C","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":"Q4928443$E05527BA-5AD5-47D0-B742-F249FE50B336","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7347d5ead75a8fa3be07f7497c38f93d8c0b5f4f","datavalue":{"value":"https://doi.org/10.1007/978-3-642-38574-2_18","type":"string"},"datatype":"url"},"type":"statement","id":"Q4928443$9870D61D-8412-44B1-AEB5-D15459310ACE","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3fc5886b5bbe009aa902975f60f2c403c867772d","datavalue":{"value":"W49696946","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4928443$09900930-55C8-4C19-91F7-447364A78DCC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"da0657b25dcc4d374ea3510625bc156a46f79a85","datavalue":{"value":{"entity-type":"item","numeric-id":2964467,"id":"Q2964467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9bb33e0d37240a44841931d15af0e6a629d10723","datavalue":{"value":{"amount":"+0.7611353397369385","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":"Q4928443$1030A855-7A09-4931-819D-7148B65C8781","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3301eaabd8b9cecc3120b315096a41a88aa00005","datavalue":{"value":{"entity-type":"item","numeric-id":5327336,"id":"Q5327336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4d2c76172b2210ed3e8c804156774caf697fcf96","datavalue":{"value":{"amount":"+0.7566643953323364","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":"Q4928443$2964ED7B-BCB0-414D-B4AD-2EB536CD8965","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":"f79bbe00b90886a771ee172bbe617b67af5077f4","datavalue":{"value":{"amount":"+0.752192497253418","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":"Q4928443$645B683D-DFB1-4B9D-BE93-A0F01F0435F4","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":"bee9cdbbab60c3e7999e9c2adbf7c4c5486bb5b9","datavalue":{"value":{"amount":"+0.7512802481651306","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":"Q4928443$706FF091-92F8-428A-B104-012FF1869EAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1335255e53437e5ef4f817148c595db6c02a4ba8","datavalue":{"value":{"entity-type":"item","numeric-id":3024890,"id":"Q3024890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9ac37eba2aa0dd5e8d0e431fc9fc568afd981a25","datavalue":{"value":{"amount":"+0.7492092847824097","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":"Q4928443$F81E0841-6D8A-4493-A9B0-DF90F3D9AA42","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4928443","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4928443"}}}}}