{"entities":{"Q5327372":{"pageid":7356946,"ns":120,"title":"Item:Q5327372","lastrevid":41552475,"modified":"2025-05-05T19:04:06Z","type":"item","id":"Q5327372","labels":{"en":{"language":"en","value":"Steps towards Verified Implementations of HOL Light"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6196187"}},"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":"Q5327372$838D1AD4-52DC-4EC5-A708-EEF54A837E28","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e090939b1b2fbcf3c45e719c6f32ea28ad15f5f6","datavalue":{"value":{"text":"Steps towards Verified Implementations of HOL Light","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5327372$DE48190E-1917-4923-BB08-A97D18AE86D5","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"99259d17b53467ae055f6ff87f0f35d2aa3275c9","datavalue":{"value":"1317.68225","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5327372$F9DC7DB0-9A26-4738-8645-1322D6C27136","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"63433eb74cec0d902b9ba62b8055b4d16f8efbc2","datavalue":{"value":"10.1007/978-3-642-39634-2_38","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5327372$88A73831-9504-4C34-B3B9-E0571B90B3CA","rank":"normal"}],"P16":[{"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":"Q5327372$633693D1-EB27-44C5-950D-410EE36E1CAA","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":"Q5327372$BD9F7028-5382-440A-AFCA-7127084DF691","rank":"normal"},{"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":"Q5327372$328E351A-BB2B-4046-9CD3-C2F3A6F7CD00","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":"Q5327372$A6E86239-C19E-489A-AC8F-0FA9975DC1A9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"00eca6587536a1681b3f41d63f34e248b2e37166","datavalue":{"value":{"time":"+2013-08-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5327372$F4ED5FD0-9CC1-4C30-A546-038F2BFD312E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5327372$45BA2EDD-1E1A-47EC-BDE7-3DA130DADC52","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ed6350364b1a982e2945715cfa9c1fc5bd3af3cb","datavalue":{"value":"6196187","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5327372$E2C50422-719C-4EEB-A290-3446CF67F10F","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":"Q5327372$D33D2220-DDBE-4B3E-85A3-323C8D1E3634","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":"Q5327372$24CF2411-F714-4DEA-8D81-1007DD3B79BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e079f4640d565f0ca1930fd327c2c7e8d634508","datavalue":{"value":{"entity-type":"item","numeric-id":21954,"id":"Q21954"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5327372$E6C306A8-8F22-42AA-963A-90152E80338A","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":"Q5327372$5D976284-720D-426D-BFB9-B77E93F9C268","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":"Q5327372$90675068-EBB9-4EEB-9AB2-BFFA3C409DDF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b06c7ac17ef3906bff6dc6958f7c3533f66da4ab","datavalue":{"value":"https://doi.org/10.1007/978-3-642-39634-2_38","type":"string"},"datatype":"url"},"type":"statement","id":"Q5327372$05FFA8AF-8797-46D3-A466-21A977A4ADD0","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"cefc5513d9cecf7ff53d185aba8db1eaf7bac406","datavalue":{"value":"W1712305647","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5327372$61320FD0-EE17-45A4-AFB9-81C725E8B8C8","rank":"normal"}],"P1643":[{"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":"1b928a37aa75e0f20da30fae987788859df1fcf2","datavalue":{"value":{"amount":"+0.9181725","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5327372$E9040B95-0147-471D-87E3-FBB8E49489D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6d7b6db4bf1924f8f4a4c27ad57224e0a8f56529","datavalue":{"value":{"entity-type":"item","numeric-id":2423767,"id":"Q2423767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"23ed4013659f59439bef55ac0b966871c81414ae","datavalue":{"value":{"amount":"+0.82808584","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5327372$BB5823D8-5796-43E9-A535-153B051EB516","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":"8902bd049253533ca1f839cedd4cabac9ce70bf0","datavalue":{"value":{"amount":"+0.8278897","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5327372$8BD26E40-95B9-48FB-BD97-DF210D6FA7A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"de9c73403d170fc9547196e85568fc9043b785b3","datavalue":{"value":{"entity-type":"item","numeric-id":3453133,"id":"Q3453133"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9c65605f6de2116dad3273ce8cef64651b8c93ca","datavalue":{"value":{"amount":"+0.8277833","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5327372$C12BDC48-3045-4E3D-9DC4-8D8A3C8330FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ecaa33f59d7da2d63f62f7085605bb6ffbbf5115","datavalue":{"value":{"entity-type":"item","numeric-id":3088006,"id":"Q3088006"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7512c61a32b13c7a3717fdee81af3a2980e38232","datavalue":{"value":{"amount":"+0.82453537","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5327372$7BFE56BC-E5E6-4A41-8111-C4CCAFEB0E24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad617f4867ba25c0dbef4c11fe4a2485819f46b8","datavalue":{"value":{"entity-type":"item","numeric-id":5869574,"id":"Q5869574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a248529144f70829855706001ff182eedd20d83b","datavalue":{"value":{"amount":"+0.8237363","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5327372$45825894-5156-40B0-B90E-B8263CADDC20","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5327372","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5327372"}}}}}