{"entities":{"Q1687723":{"pageid":1698464,"ns":120,"title":"Item:Q1687723","lastrevid":52984493,"modified":"2026-01-23T23:26:12Z","type":"item","id":"Q1687723","labels":{"en":{"language":"en","value":"Formal verification of a floating-point expansion renormalization algorithm"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6821846"}},"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":"Q1687723$464B9D7E-17A5-45EF-98D3-018000B935F1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"29d13c455195312af27c6a836ca3511ffb15b207","datavalue":{"value":{"text":"Formal verification of a floating-point expansion renormalization algorithm","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1687723$67171CF9-9BD1-4E4A-B244-0F8D7BC2C775","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"098953e2162e75796e68a7e61d4e6034f9a559c4","datavalue":{"value":"1483.68479","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687723$615FE1B3-8451-4E8B-BC14-4B212FEFE61B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"642075ee40d863e242b359a1cffce37539d22286","datavalue":{"value":"10.1007/978-3-319-66107-0_7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687723$E14BE21A-F5E3-4667-B08D-87F5DFE65B8D","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":"Q1687723$615F6891-75AB-4C7F-90A7-D03B92C7D7DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2ce11399fb21c03553c80196877b5dbb355c67d0","datavalue":{"value":{"entity-type":"item","numeric-id":1687721,"id":"Q1687721"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687723$9BB39213-4535-4ED4-8C75-F351E9083D55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"81a226bb8cb4f6ca735813db79e1c23942b1542c","datavalue":{"value":{"entity-type":"item","numeric-id":342872,"id":"Q342872"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687723$8998323D-BA38-4D68-9FBC-4309C5BB2BE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4f6bb7f4a043df05cb674cfe2f11e90108ac1100","datavalue":{"value":{"entity-type":"item","numeric-id":1687722,"id":"Q1687722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687723$EB10DBB3-ED99-4360-9BAF-EF6003A5E8A6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7600255b4ee907c1b1dfbc5f62c7b1165ab1b6d0","datavalue":{"value":{"time":"+2018-01-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1687723$93A79718-71DC-4BDE-AA17-1F57E5EF46A8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687723$0A21111B-E0F1-4CEB-8E45-E9FB0B0689ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"235c6ea5e302e28be6b7d95307dac1a9f1d2b5b4","datavalue":{"value":"65G99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687723$5F443174-0B4E-4B12-BD50-C33736D52A6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a61c1214f17b12b67364674d8143dbdd872c34c1","datavalue":{"value":"65Y04","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687723$29B6DC1F-8AA8-4059-9A48-5DDD5A03D484","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"41ba4cb48b32bd27fb319d4bb9e02a7acd0fd4e2","datavalue":{"value":"6821846","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687723$8C2AA303-E05A-418A-A5F3-9D9E3104B9E8","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"00216556e27ad3bbc2d642874d0693b52d5f53d1","datavalue":{"value":"floating-point arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1687723$2E683F65-3A6E-480D-B6B1-678E031CFB9C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"037ee4079c9987ed7f8e30aeddcd9f04e53c8b14","datavalue":{"value":"floating-point expansions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1687723$973394B6-2662-443B-ADBD-874E59D7D8EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"afb1016fd318f4f8e8efc7a4bb577f29552441ee","datavalue":{"value":"multiple-precision arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1687723$1EBCF898-7901-4A3D-A137-AE73D0584551","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"326c300cf62efa849a7bdb94dd90663d744d9f5d","datavalue":{"value":"formal proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q1687723$2997AA03-D165-4011-BBAE-A490D498EF6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q1687723$1A5C774C-EF4C-4AF4-AE7C-6B11C5554C67","rank":"normal"}],"P1463":[{"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":"Q1687723$DAF5A2BA-31C2-4932-AAA0-F72F7A4E758C","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":"Q1687723$BB9D97F9-ADC1-4BCF-A054-E55AA088EBF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c0b499821f3ec8e09ffa8d9ca0d3af779a5b4920","datavalue":{"value":{"entity-type":"item","numeric-id":15844,"id":"Q15844"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687723$C74E4D66-1100-4069-8742-ED5DE1371984","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ca4b988836553ae700f573bfcff706becca8c70b","datavalue":{"value":{"entity-type":"item","numeric-id":27049,"id":"Q27049"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687723$816138D1-DE26-4F42-953D-C2FC58615737","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":"Q1687723$08B4BDCB-729E-46C1-B20C-B09DD19F3F13","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"701319c0f73092dea375084d7bfc71a7ad4146ed","datavalue":{"value":"https://doi.org/10.1007/978-3-319-66107-0_7","type":"string"},"datatype":"url"},"type":"statement","id":"Q1687723$9147B53E-0F21-4E72-A9D3-A04069942E40","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5652675f992991c4d648652cb6339907da9d6a8e","datavalue":{"value":"W2736053689","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687723$34D110B5-F443-4E05-9788-30AC55CCEBEC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8c535b8eea6a270b85018e407775c2f70f97646","datavalue":{"value":{"entity-type":"item","numeric-id":2352948,"id":"Q2352948"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687723$11C3BF34-5CEB-4E04-891D-C6BAAE069908","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"20cc166be703e3232a5043f2b94d3d8da0133903","datavalue":{"value":{"entity-type":"item","numeric-id":3549209,"id":"Q3549209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687723$645F3A89-3BD0-4C01-8931-E108C9DAAD95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"29380d76dbcbce79ea3c9a693d7306e686c6a71c","datavalue":{"value":{"entity-type":"item","numeric-id":2848614,"id":"Q2848614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687723$8977F9CA-227A-4AB6-B78E-AC2DE1246D11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7c38af934d463d4d09550b047af6aeb2bbe1a285","datavalue":{"value":{"entity-type":"item","numeric-id":2985528,"id":"Q2985528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687723$083DDA2E-9981-49A9-8BA2-E1505A6A1549","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"28afd2fcb541e36a9b490796fab49ed4b5aabc61","datavalue":{"value":{"entity-type":"item","numeric-id":2819222,"id":"Q2819222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687723$4A32735C-B874-4B62-8E1C-A55864779F1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6629b8e6f8d9ab97bd201da69f9559dbb3ecd9c1","datavalue":{"value":{"entity-type":"item","numeric-id":5277636,"id":"Q5277636"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687723$F9C3676D-B6BD-4055-82E2-5E1B5B7D30E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d077f7417b2812e541ae3d63f2b9abb351153146","datavalue":{"value":{"entity-type":"item","numeric-id":3629031,"id":"Q3629031"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687723$052AEEEF-7966-403F-A0FD-6E0F5A84BD22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ac6818aeffdaf8415a5a7f081a2da5ee7312891d","datavalue":{"value":{"entity-type":"item","numeric-id":5693174,"id":"Q5693174"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687723$8FCB9C59-EADA-45FE-805E-984EDDCFB9A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"32a89a983fb03b95f29a4dd8d8dbfee04649210b","datavalue":{"value":{"entity-type":"item","numeric-id":5189669,"id":"Q5189669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687723$22B0697E-23CF-49E8-8273-6FF0E3EA963E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"08972496f8d06b458c2cad3d9db4a9e4afb31659","datavalue":{"value":{"entity-type":"item","numeric-id":1380822,"id":"Q1380822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687723$041E1EB2-B5A5-4C40-9F90-9E35720D6506","rank":"normal"}],"P1643":[{"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":"aa018c7264a4a3e583be0825f7156b0a7c5a3951","datavalue":{"value":{"amount":"+0.7567769289016724","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":"Q1687723$F28863FF-FE11-442C-9043-93AC2C612CC3","rank":"normal"},{"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":"4bfb350cad0e8d66b299f2a1272b1c7d57ec77f9","datavalue":{"value":{"amount":"+0.7537469863891602","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":"Q1687723$5FADDB3B-6E1A-4648-9483-BDEABE8AF1E7","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":"326c8e5f75a7a17afa33b392651f70e6c7613fa4","datavalue":{"value":{"amount":"+0.7451881766319275","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":"Q1687723$0A2436D3-2DA5-4198-914C-854807459E58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"82c6e281486ce3a8d3bf6567f793e08c8232cf8b","datavalue":{"value":{"entity-type":"item","numeric-id":2723405,"id":"Q2723405"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a07cca6644a04fec1660a2138b7f9e32295804ad","datavalue":{"value":{"amount":"+0.7358493804931641","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":"Q1687723$C55B584A-386E-4D1E-9028-B492F0539059","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"39838fc97364315b097b7b3e6cbac1c2be6af363","datavalue":{"value":{"entity-type":"item","numeric-id":5086229,"id":"Q5086229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"030c36d77c17b43331fd09cdd3bfc74ec2534da8","datavalue":{"value":{"amount":"+0.734586775302887","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":"Q1687723$CDB8ECE1-43A1-4579-8E7C-6BD466B41210","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1687723","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1687723"}}}}}