{"entities":{"Q2520685":{"pageid":2531428,"ns":120,"title":"Item:Q2520685","lastrevid":74168895,"modified":"2026-04-14T18:46:12Z","type":"item","id":"Q2520685","labels":{"en":{"language":"en","value":"A parameterized floating-point formalizaton in HOL Light"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6664855"}},"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":"Q2520685$CBE7B677-8642-44E9-8368-4F0EBD56C44F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9c1b15c493e73be265827ef0ee5150e2791c9b55","datavalue":{"value":{"text":"A parameterized floating-point formalizaton in HOL Light","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2520685$21A3E71D-59F9-4892-9BEB-7AD832EB6DA6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"79a5ef18c5eefff311e62ec7a1f6e37adbb7b8f5","datavalue":{"value":"1352.65667","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2520685$E5945A4E-C874-4193-8FB2-B286AE8641CC","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d947f67d994fe555ea4420978a2eb1be3f098bc3","datavalue":{"value":{"entity-type":"item","numeric-id":2520683,"id":"Q2520683"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2520685$C5BE4DAA-E6FB-4A9B-8DC4-886996C9A415","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8dd5f0e818e272e3a2ec7bd09ea12e648a41f648","datavalue":{"value":{"entity-type":"item","numeric-id":2520684,"id":"Q2520684"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2520685$62960F25-6147-4F91-B354-A5EF66280AD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6bb25cd5bff61dd98c69faa32322d3d5f5b3963d","datavalue":{"value":{"entity-type":"item","numeric-id":239161,"id":"Q239161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2520685$0A0319EB-62EB-4600-863F-6BAAC3A247DD","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"81dc7daf8e9d74fc43b1651d3815e34e62e970ab","datavalue":{"value":{"time":"+2016-12-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2520685$B0959ACA-8DFC-488A-9903-581145806502","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a61c1214f17b12b67364674d8143dbdd872c34c1","datavalue":{"value":"65Y04","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2520685$21C0EA22-C821-4D26-8B54-35B4381EB876","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"224133dd68a4f3b66ddf7d50fd627018c06684e4","datavalue":{"value":"65G50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2520685$F47F08DD-F9CE-4FA1-AD5F-99F0571AC358","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2520685$E2B8BF98-F6E9-454D-844B-C6C412912BEE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0aae7e02e3170b2a83d4d5421a843f96beebcb0c","datavalue":{"value":"6664855","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2520685$AA9F66B9-3613-4649-A767-91408AE251AE","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb4356ad2cd61bb5c06e07f06467b4254be8c7ea","datavalue":{"value":"IEEE-754-2008","type":"string"},"datatype":"string"},"type":"statement","id":"Q2520685$5569AA67-3834-49C7-9C51-9FDAD02E4E0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"00216556e27ad3bbc2d642874d0693b52d5f53d1","datavalue":{"value":"floating-point arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2520685$1BCB2EF6-8DCC-4223-8612-0DB5397F1A1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f6ae68baccf633ba093eff10bdee5004dd85fd95","datavalue":{"value":"fixed-point number","type":"string"},"datatype":"string"},"type":"statement","id":"Q2520685$D7E43236-B8DA-46C4-AC18-CC4A9081E1E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d5ef51b89dbf72f7181f6b41896d9233a3e6b1ce","datavalue":{"value":"formalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q2520685$FCE06DD8-B032-44BD-87A8-C69D54ED4F7E","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":"Q2520685$4FE8E681-BB2D-4315-8B34-57C8594EA5B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c652637493e8de65377ba80065ca4183c6dc627","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2520685$8370F76D-F41D-400D-A4C2-0B8C7C6EC081","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":"Q2520685$E2715C15-1BBE-4B5F-9104-432CB6F18121","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e338912f65cbd77347bbd512933e55736ef58bd1","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2520685$E26323F6-DC26-4D22-88CA-7EE6138F7474","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3cbae6652830cce326cac236409178e713b609d8","datavalue":{"value":{"entity-type":"item","numeric-id":43932,"id":"Q43932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2520685$664363EC-6FB1-4FAE-A273-221AD9343E80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f3a054baa4efca75beada6ac9f2f664c52ac32a0","datavalue":{"value":{"entity-type":"item","numeric-id":15791,"id":"Q15791"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2520685$1D8E4FAF-115F-4117-9262-DB6B6E218467","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bcd2724f6e8447a24419ed553b7520f7a96db016","datavalue":{"value":{"entity-type":"item","numeric-id":16194,"id":"Q16194"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2520685$527EFDE4-6370-4E8B-BA49-5D1C8F647A5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"aa786b5c8269f6cf517ad0f032932817c0bb268f","datavalue":{"value":{"entity-type":"item","numeric-id":18875,"id":"Q18875"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2520685$A898DB16-4F29-4FBA-A623-03AA4BF28B85","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":"Q2520685$8718062F-1AFD-4020-AD38-1674ECA83447","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b7a4d7ad399d4646eaed622234f957e832bbd5b7","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2015.10.010","type":"string"},"datatype":"url"},"type":"statement","id":"Q2520685$A5DB4FF1-D707-4940-B320-F92E488CC26F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3a5c57896dbfdc39365d1b648abc289957453260","datavalue":{"value":"W2251636819","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2520685$FAA3443A-C54E-4F10-AD51-35459B99C053","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"9e0a5c6d3f5d7d176e727359cdd51207ac065ac6","datavalue":{"value":"Q113317760","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2520685$4E25D4CA-B8B5-415D-949B-D58BF0B31FBA","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ea93d70d0843219931b720e4d82e67b9e625b79","datavalue":{"value":{"entity-type":"item","numeric-id":4975005,"id":"Q4975005"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2520685$03346582-A73B-4E6F-A7C0-24D0C242AF08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a2940d495eb2b669794d95ca8ddbb03437430e8b","datavalue":{"value":{"entity-type":"item","numeric-id":4790659,"id":"Q4790659"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2520685$B80845CE-2FC9-4D23-AD2F-3653951C69D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d72e60cd5753f5e8a10ea2d01659548c99516e9d","datavalue":{"value":{"entity-type":"item","numeric-id":5498687,"id":"Q5498687"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2520685$CD704213-DDF7-482E-9BD8-B0DC1618BC6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5a462f97a14149f26095e85bb29dcdaa29aa187a","datavalue":{"value":{"entity-type":"item","numeric-id":4949347,"id":"Q4949347"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2520685$FDC9D47B-FA5B-4C60-A7A0-169562AFF7F3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"290e0d95ef1f64eafa721c6f84d61af4da9a89cc","datavalue":{"value":"10.1016/J.ENTCS.2015.10.010","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2520685$F2E5F3AD-9BAC-45FD-AEC2-D4BF2AD9E5CD","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ac0ce1a15a6f8a98914f6aa448f055825b864ff2","datavalue":{"value":{"entity-type":"item","numeric-id":714617,"id":"Q714617"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3596634aa4ab09df634840419b684bb4f241a978","datavalue":{"value":{"amount":"+0.7844537496566772","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":"Q2520685$2D0F3773-563C-46AD-8ADE-A6284C1D297D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b97311b85d17b368c78a2ea6a875377f7441a650","datavalue":{"value":{"entity-type":"item","numeric-id":816219,"id":"Q816219"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"74f3cc736f38ddeaee319850d26050e3de788130","datavalue":{"value":{"amount":"+0.776393473148346","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":"Q2520685$916EC74F-01A4-48AD-B395-FDAEED3CE916","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d3f9e9873cfe4644b6583f05111df3e873bf45d8","datavalue":{"value":{"entity-type":"item","numeric-id":5274886,"id":"Q5274886"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4a512eb8a187dfa29bd2c19512c7d76245df7047","datavalue":{"value":{"amount":"+0.7637019753456116","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":"Q2520685$B031C7F5-FB25-47E6-9ADD-6A984D1B5526","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ec27229d4d40b3d0ec7ab4f58cd498117b180b8a","datavalue":{"value":{"entity-type":"item","numeric-id":4790659,"id":"Q4790659"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3ca73cd620ad17d6c7dc90eee5c582e2960fa356","datavalue":{"value":{"amount":"+0.7557287812232971","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":"Q2520685$9961D79E-6FDA-4C9C-9EE9-2BDA7DB1D6BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2136fb2592385d1514bfed4dfbe97047eade54b0","datavalue":{"value":{"entity-type":"item","numeric-id":4737560,"id":"Q4737560"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b3c14c02a518ea85d3be03f2a47b83f12558b27f","datavalue":{"value":{"amount":"+0.753545880317688","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":"Q2520685$497981D7-E35F-4D4E-A5B6-CBF9322AE608","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A parameterized floating-point formalizaton in HOL Light","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_parameterized_floating-point_formalizaton_in_HOL_Light"}}}}}