{"entities":{"Q5274886":{"pageid":7304461,"ns":120,"title":"Item:Q5274886","lastrevid":52847186,"modified":"2026-01-23T15:31:47Z","type":"item","id":"Q5274886","labels":{"en":{"language":"en","value":"Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6740638"}},"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":"Q5274886$A66232BD-2822-4C5C-AE17-C8EDB5074A46","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6c406c4a0e29f5ed667a670f365ee30cc79ca6b5","datavalue":{"value":"1385.68001","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5274886$05D1EE0E-AF52-4D73-97F1-928D55093725","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"55cfbbbb889685c16294bfa3437f02f1746fc983","datavalue":{"value":{"entity-type":"item","numeric-id":352947,"id":"Q352947"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5274886$F7B0C1F5-2C50-4CC4-BCDF-38137405C333","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5cbf89c19e1c3435f0c553619d3746d84ce08e7f","datavalue":{"value":{"entity-type":"item","numeric-id":331614,"id":"Q331614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5274886$CB83DE48-6AD8-41A1-B85E-751807AA415F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1a7c9d02f6a4a594410711d22dd1a021deb4336e","datavalue":{"value":{"time":"+2017-07-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5274886$3FADD97D-5EB9-4396-A29D-503F81DB152C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2c7d886bf784cedc728047b558b8229366192cbf","datavalue":{"value":"https://www.sciencedirect.com/science/book/9781785481123","type":"string"},"datatype":"url"},"type":"statement","id":"Q5274886$93318A11-1223-4468-88AD-93B1BBBC8D36","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"24aafcf24a21bd70cd3b62d3f5f72a6d0d82d816","datavalue":{"value":"68-02","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5274886$853D846B-9CFF-4500-B6A4-87E6936339A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"224133dd68a4f3b66ddf7d50fd627018c06684e4","datavalue":{"value":"65G50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5274886$10B0D8E9-183C-4AA1-8601-95ACA8712D24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a61c1214f17b12b67364674d8143dbdd872c34c1","datavalue":{"value":"65Y04","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5274886$87C6D198-C23D-4F76-A6AD-3DD53B2B8842","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5274886$EC85D792-9C69-4B64-B8F7-1CB0A398EC5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5274886$4582FC02-D096-4A5A-8296-FC78E87A6077","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"147b91ce07b32ef8039e4ea024cd9b4568492dea","datavalue":{"value":"6740638","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5274886$FEC70346-48D7-4160-877A-840056E78B0C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"00216556e27ad3bbc2d642874d0693b52d5f53d1","datavalue":{"value":"floating-point arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5274886$5ABEE5FB-2D70-4DCE-9192-2C1CAC8EB31E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"326c300cf62efa849a7bdb94dd90663d744d9f5d","datavalue":{"value":"formal proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q5274886$3C852007-FBA1-41C7-944B-C426BBB525FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q5274886$7947E6C7-ED8F-4BB1-8084-CB3969DD357B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q5274886$7A52DDEE-96D0-4863-93D3-83FC86BC0688","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"84eefd31cc35b0f322abc9d88353a26c9605ee67","datavalue":{"value":{"entity-type":"item","numeric-id":23492,"id":"Q23492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5274886$29BFBA38-64BF-4B5C-AD3B-DE898B6BE68B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"86f3dd89cea99e36ca0370b5d16e0fd864711e2c","datavalue":{"value":{"entity-type":"item","numeric-id":17037,"id":"Q17037"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5274886$14F571FC-475D-4E13-846A-8E349CBC5CDF","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":"Q5274886$3BE87E76-C084-45A4-BFA0-7D7C5919BB39","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":"Q5274886$8BB88319-9735-4115-A118-3B1F5932459A","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":"b0ae9104efc4695a8c3a24c3e042a00b16144aee","datavalue":{"value":{"amount":"+0.8618346452713013","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":"Q5274886$17F6F442-622D-411E-9A89-B7EA68C799AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"87ee57d522e3c062e63865eab020bcf1c5c31db2","datavalue":{"value":{"entity-type":"item","numeric-id":3629031,"id":"Q3629031"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7abe03ee3f6e551a93e6b595601e34562437ee29","datavalue":{"value":{"amount":"+0.8593622446060181","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":"Q5274886$1549F76E-BCD7-43CE-83E8-09AA669A7F62","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":"c258646c02852d6f55f6047ca6acbeab679aac39","datavalue":{"value":{"amount":"+0.8150461316108704","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":"Q5274886$E0730FD8-F7AF-4BD4-9599-0E884C939406","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"39543e823be30e37369ab04509198db83e3988ed","datavalue":{"value":{"entity-type":"item","numeric-id":2352505,"id":"Q2352505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"11fbc9f81b9748256bd0ab1a4be54df688c495dd","datavalue":{"value":{"amount":"+0.8085635900497437","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":"Q5274886$E9E8F3DF-D7DE-40FD-962A-A384F4DEB0AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"693844e8eae80a91abc67434d7d59fe9c34b67c5","datavalue":{"value":{"entity-type":"item","numeric-id":4011800,"id":"Q4011800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3072d015673ae450c96bea41223a71cd1c82452d","datavalue":{"value":{"amount":"+0.8018279075622559","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":"Q5274886$DC411E55-904D-4BDA-BFCF-D9CCC0989B83","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5274886","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5274886"}}}}}