{"entities":{"Q2879260":{"pageid":2889980,"ns":120,"title":"Item:Q2879260","lastrevid":52085366,"modified":"2026-01-20T22:02:50Z","type":"item","id":"Q2879260","labels":{"en":{"language":"en","value":"HOL with definitions: semantics, soundness, and a verified implementation"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6341489"}},"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":"Q2879260$6150E9E6-7634-43EA-9EF3-3DABB4561451","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"bcf55f1e52b042ab15f1d49e2acfcea7d047d00b","datavalue":{"value":{"text":"HOL with Definitions: Semantics, Soundness, and a Verified Implementation","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2879260$AF82BDA1-73BF-4C4A-B435-C4E1D807B84A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d97bb3d69f0a10140163fd193cfa491a7ecc5efa","datavalue":{"value":"1416.68167","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879260$DA0D424D-7EDC-41CB-99FE-B8FD3AF4814A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0ea7da0751a7a790ec4e234e20ab1840132f3a76","datavalue":{"value":"10.1007/978-3-319-08970-6_20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879260$629FF112-9079-40A1-AFB4-4BA9F7EADC4E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"62025305e3524f61b1fc8b1f7bbd2484241846ea","datavalue":{"value":{"entity-type":"item","numeric-id":287359,"id":"Q287359"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879260$18BCFF72-25B7-4214-B7F1-46F3884BEF99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a0326155ee2776709b948d74abcb135838e086e1","datavalue":{"value":{"entity-type":"item","numeric-id":287357,"id":"Q287357"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879260$03F36A6E-FA5D-438B-9C99-789E719A1C78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c330e55e5dc72ba4e46dcf35457734e0df28701e","datavalue":{"value":{"entity-type":"item","numeric-id":286789,"id":"Q286789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879260$27426705-4AB6-4207-A496-A637C9110B5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"57155b56d8fbcd7c5881cc6580886a49385bb630","datavalue":{"value":{"entity-type":"item","numeric-id":287360,"id":"Q287360"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879260$DC2C6A2C-303B-410C-9841-6D30A328BD1C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d43c6ce6e92d67a2cb7e4a7df2a7d5eeec36e724","datavalue":{"value":{"entity-type":"item","numeric-id":2829237,"id":"Q2829237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879260$0F060117-1D4C-48E1-8153-D4F322A74ED1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"565bc5987614f46e32dc98add32d630fe2eeb533","datavalue":{"value":{"time":"+2014-09-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2879260$40F7749C-A564-483C-8986-1E162E9978F3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7399e7d9d2dc4703ad0957d432f4444074feade8","datavalue":{"value":"https://kar.kent.ac.uk/38886/1/itp14.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q2879260$2C230225-0D93-4EAE-B65C-48A954651BA2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879260$7BA797C8-8753-4337-A5CB-E052AB242965","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879260$062BCD08-60DA-4352-9B72-AEAE7065DEFD","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0c5a4e288e9bfd88cf2e190d2f808ea9a133db77","datavalue":{"value":"6341489","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879260$2E0E21C8-4BEB-47B3-A791-186D82BAB60E","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":"Q2879260$3562A849-ACD7-4E8D-8EC7-A56B1962EBC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"44e192ea0614ca90dcab29c306f09db708056c50","datavalue":{"value":{"entity-type":"item","numeric-id":24736,"id":"Q24736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879260$17B62780-87B7-45A9-818F-9CADDA2ABFAA","rank":"normal"},{"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":"Q2879260$878BEAB4-4E73-4C06-9895-5C3007C248FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"533959f24a509b955614f607e46b8aa4cec190ef","datavalue":{"value":{"entity-type":"item","numeric-id":20799,"id":"Q20799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879260$574EFF3B-8040-43B4-8FE6-7288B50678AF","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":"Q2879260$690A5B32-B8A7-4C06-8968-223F82EDF312","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":"Q2879260$0EC0F169-D586-4494-BFBC-FAF364796901","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"2a431a7dba51881102c44d632c94814b0088769f","datavalue":{"value":"W2144280226","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879260$C1FE7A50-9E1A-4191-A324-E5A63F124377","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5ca6b33a9f213e3f67729583300a9e1f98b54e7d","datavalue":{"value":{"entity-type":"item","numeric-id":287361,"id":"Q287361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e6a850bc2c5af92fd3b34cde9ca422c071e9a6e1","datavalue":{"value":{"amount":"+0.8948500752449036","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":"Q2879260$A87A0E81-DCF7-4E63-8953-8C242577475F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f1cab783396284eb004b42756f108087b79277b8","datavalue":{"value":{"entity-type":"item","numeric-id":3613408,"id":"Q3613408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d92bba6e5052d29012093f7a26ef50addc51a42c","datavalue":{"value":{"amount":"+0.8422838449478149","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":"Q2879260$FD11731C-DAE1-4305-9E78-BA29E7F8D56D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8a9340227e03cb52d0a7ec16f7ac5a22cc95744b","datavalue":{"value":{"entity-type":"item","numeric-id":5327372,"id":"Q5327372"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a1fc688387a5dccb7f28a14b984fc24ccdb8e6fa","datavalue":{"value":{"amount":"+0.8345103859901428","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":"Q2879260$94FF3BC3-A618-42B2-8A6D-88C26F958173","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"08a4d9babdd0dc4f3d4a84fe7e41ccc98bd845de","datavalue":{"value":{"entity-type":"item","numeric-id":4964711,"id":"Q4964711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"391219c313ffd9fdb8e32bced19950d677073974","datavalue":{"value":{"amount":"+0.8114402890205383","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":"Q2879260$E410F92B-D2F5-4017-A410-7F1BD357348C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bd58fd6243ca5ecfa61b5100df2e972a1ed7fb82","datavalue":{"value":{"entity-type":"item","numeric-id":5458382,"id":"Q5458382"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"099753854748b3bcbb5904093c1a150838b18dd0","datavalue":{"value":{"amount":"+0.7884350419044495","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":"Q2879260$05F051F1-BB8A-4BBB-8F85-442AB41431B0","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2879260","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2879260"}}}}}