{"entities":{"Q2843014":{"pageid":2853734,"ns":120,"title":"Item:Q2843014","lastrevid":58024374,"modified":"2026-04-03T12:12:25Z","type":"item","id":"Q2843014","labels":{"en":{"language":"en","value":"Capturing hiproofs in HOL light"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6197182"}},"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":"Q2843014$B544385D-0A6D-4981-AB38-A9448BB6083D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d56db39c373c48163925b1f376bda5b2c8659796","datavalue":{"value":{"text":"Capturing Hiproofs in HOL Light","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2843014$480AF883-C3BF-4102-9230-8702A1809E23","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"fea891a8a2d52210f0982979dbe26f1923f55f71","datavalue":{"value":"1390.68583","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2843014$88BDED87-DF07-4BFE-A8D1-3E198F9B88B0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"10bea0df45aaa417f72a596319c0373b7e443e98","datavalue":{"value":"10.1007/978-3-642-39320-4_12","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2843014$6B2A7EF5-EF4E-46C4-975E-6269C802F7BD","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"14c5746c9fb7bd206dc1bf3cfc28ead272520668","datavalue":{"value":{"entity-type":"item","numeric-id":2379682,"id":"Q2379682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2843014$DA7F4CD2-BADF-41FF-A9E3-A5F3BDA53E28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b166638dd0d01a64c8692be072b1b15b38e4f777","datavalue":{"value":{"entity-type":"item","numeric-id":2829239,"id":"Q2829239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2843014$BEE435FA-4BD5-48FB-BE76-E9BB6826B62B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1cb2d83c6e9a26863f5eadd24ed7ef714112a42b","datavalue":{"value":{"entity-type":"item","numeric-id":626930,"id":"Q626930"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2843014$8B71A373-7FCB-477E-AF07-37517281D5D2","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":"Q2843014$A1A632FA-B686-4D46-B799-28C88ADC7400","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"381d46b885a4d4a1524f419ca9a0dc18cd8f863b","datavalue":{"value":{"time":"+2013-08-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2843014$3DC5D29E-0EEA-4A12-99AE-3702DA64EDBC","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"71638f44b8ea28b23c75f07f1f12741a0b5a8a48","datavalue":{"value":"https://arxiv.org/abs/1307.2713","type":"string"},"datatype":"url"},"type":"statement","id":"Q2843014$4462DC2B-8D6C-4BCE-BED3-BA9883825B38","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2843014$D961FA15-B34C-4558-B1C7-4DD904023171","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b8982b79dcc64717efe32d4280c416c6c8799ec3","datavalue":{"value":"6197182","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2843014$BD492257-A171-499D-BF0B-886AA86CA0DF","rank":"normal"}],"P1463":[{"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":"Q2843014$28B1E2B6-D43C-4A05-8B87-0979A0CA43DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"62ba86aa6537435eabbaebc8bfe3b9fc42cedbd1","datavalue":{"value":{"entity-type":"item","numeric-id":29448,"id":"Q29448"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2843014$8B626F95-F635-47FA-843B-CCCE5E25B2BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"38f7499dd729e9adcd6e9f5ac051cd1e46e19f42","datavalue":{"value":{"entity-type":"item","numeric-id":29449,"id":"Q29449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2843014$9D95F38F-6A17-4939-9E75-B48C48431F3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d5059e524c0bc27ec6b92bffb4fed95b952c023f","datavalue":{"value":{"entity-type":"item","numeric-id":29450,"id":"Q29450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2843014$E604E186-6FB9-410D-8AA8-1D8F394DC553","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":"Q2843014$68AA715D-1B4A-464E-A5E0-F807CE4F90C4","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":"Q2843014$DD764F7F-EFF1-4C73-90FD-924D050952A7","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c5ebc3f68ecc1b68868cab2a9b8fbc6342677a2c","datavalue":{"value":"W1842581062","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2843014$D074AC13-6E29-45D7-8FE1-7F509910A168","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cc534be3eb834aabf0b2f4a9c4c155267b2fe28e","datavalue":{"value":{"entity-type":"item","numeric-id":2852358,"id":"Q2852358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"de4d878525387230df2e447e6882e7d0c263714d","datavalue":{"value":{"amount":"+0.8707189559936523","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":"Q2843014$97E0893F-8D01-4DE6-801F-E52E143E8355","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"09aab0dad9dd5b10f6c7792ef99e86573d003dbb","datavalue":{"value":{"entity-type":"item","numeric-id":626933,"id":"Q626933"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"75a613a7cff80226f6254187f515ef7e742a0d74","datavalue":{"value":{"amount":"+0.8051263689994812","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":"Q2843014$AECFF9B4-F44F-4814-A95F-CA3C419DC356","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cb96d09cfe6e95409cf59d2778d0c56f05ba4e0e","datavalue":{"value":{"entity-type":"item","numeric-id":5505516,"id":"Q5505516"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e149c4ddccde94dab86cb1d77816344a3ad1cf85","datavalue":{"value":{"amount":"+0.767465353012085","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":"Q2843014$BA084346-290B-4BCE-B915-C46F0D23396A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3544d3ba92bb4a6d43ae5a936bf62ec439806db3","datavalue":{"value":{"entity-type":"item","numeric-id":4928443,"id":"Q4928443"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6469d53e089a114df4877b4fc23d06f1d20daf00","datavalue":{"value":{"amount":"+0.7340794205665588","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":"Q2843014$21CA7F7A-EF14-49C2-BDDB-41EE28EF0274","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":"ef9d4adb3789115cc5181dbf0c99919540810c9e","datavalue":{"value":{"amount":"+0.7259137630462646","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":"Q2843014$AD289DAB-FF5E-4769-9F0F-B47F7C254BF3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2843014","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2843014"}}}}}