{"entities":{"Q2164244":{"pageid":2174987,"ns":120,"title":"Item:Q2164244","lastrevid":54381317,"modified":"2026-01-26T17:52:00Z","type":"item","id":"Q2164244","labels":{"en":{"language":"en","value":"A three-tier strategy for reasoning about floating-point numbers in SMT"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7571388"}},"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":"Q2164244$C63CA2F0-5ECD-4A9B-BC89-F37FF47277A5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"dd574e45e165a22a7b3ac72c9679b0f597df27b6","datavalue":{"value":{"text":"A three-tier strategy for reasoning about floating-point numbers in SMT","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2164244$9FD3869C-01A9-4A1A-B5EF-9CF60EAF22EF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"175e02c91c83ead08839b5bbf780e22be7c9099f","datavalue":{"value":"1494.68282","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2164244$888F6874-2515-4C5B-A422-1462C2CB6CBD","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7140b00bcdebfdf877abfa47a163594bacbe3245","datavalue":{"value":"10.1007/978-3-319-63390-9_22","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2164244$73BAB5BB-4C07-45EE-B5D1-B37BCEAB4B59","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"2a9c3e977eb61b9fc5b2fcb92fe6e8ddc0a12670","datavalue":{"value":{"entity-type":"item","numeric-id":287381,"id":"Q287381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2164244$E0BC2D76-505D-451C-A914-CB6C30D0660E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3a4cd5b7469d05395148ef8e57efa9461416d131","datavalue":{"value":{"entity-type":"item","numeric-id":2164242,"id":"Q2164242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2164244$4DF26514-85C5-4919-9EDD-F83DF2D9A601","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b8d8a94af8132629fb82e400d7364ab62a1388a4","datavalue":{"value":{"entity-type":"item","numeric-id":2164243,"id":"Q2164243"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2164244$93541DA9-BEC2-4621-9D8C-6E3168BA97E4","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":"Q2164244$E6177717-49BD-48A7-8C2E-5EDC2FCB317E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e7c6924ad0a88ab7e054b45d5b003a84c37d69f2","datavalue":{"value":{"entity-type":"item","numeric-id":1630032,"id":"Q1630032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2164244$8ACDE46C-1DB0-464D-BBD9-78A556767C03","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7aa7040e0858a957251ee78ad1edc7d13d61d833","datavalue":{"value":{"time":"+2022-08-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2164244$45A2DDFE-A86F-476A-9EDD-9B5D9A9B500B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"217e9d437108948005ddd352d459ebfbc900bf92","datavalue":{"value":"https://hal.inria.fr/hal-01522770/file/main.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q2164244$F213F529-D071-4A5A-AC74-00D7BB54CC6A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2164244$CFE40CF2-E144-4532-A610-140E98938054","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"224133dd68a4f3b66ddf7d50fd627018c06684e4","datavalue":{"value":"65G50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2164244$B0746CD3-FF32-450F-91C4-4E9A675317A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a61c1214f17b12b67364674d8143dbdd872c34c1","datavalue":{"value":"65Y04","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2164244$7ED18F34-587D-422C-A383-82A4B8318259","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2164244$4B5F1E2D-C3D9-491F-87A7-F9105698624C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9b74f00e730242f625955368133b518ade02cbcd","datavalue":{"value":"7571388","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2164244$6906846F-9292-4A70-A3CD-C810375F690F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dc37cf6bf1a4fd159f089028e999146e64828fa8","datavalue":{"value":"SMT","type":"string"},"datatype":"string"},"type":"statement","id":"Q2164244$1325138F-F71F-4537-AD63-B6D835D4BD36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"00216556e27ad3bbc2d642874d0693b52d5f53d1","datavalue":{"value":"floating-point arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2164244$F5E94E80-D5A1-4CB5-80BE-76A67F8B5D1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2164244$A3CD9C8C-4AA7-4548-AEB0-FB4D6507D75F","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":"Q2164244$E62F12EB-250F-4F8C-A5BC-B345A13666E2","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e8be6ec3916156f5a4ea2317e0f2c8bb1236d820","datavalue":{"value":"W2638593226","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2164244$802A2C32-FD03-420D-869E-B0F4B5005781","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ae543d3164609a478eaf3c26694eec20cce9b473","datavalue":{"value":{"entity-type":"item","numeric-id":479837,"id":"Q479837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5a90f8127ab979022be82b8e38e340aa7801453a","datavalue":{"value":{"amount":"+0.7676745057106018","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":"Q2164244$27CD78C8-725D-4DF0-B79B-F996912D0DC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a95aaea7a91a11e558a80cfd0d298e5e5edec5b3","datavalue":{"value":{"entity-type":"item","numeric-id":3636881,"id":"Q3636881"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c7125d2fecb1d69dec6367c3a1e1ac4100453d92","datavalue":{"value":{"amount":"+0.73566734790802","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":"Q2164244$44EA426F-5A4A-47D5-952A-6C40F624BC5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"006e26d9ab846780e23445f97dcf8eca0df10f00","datavalue":{"value":{"entity-type":"item","numeric-id":1799086,"id":"Q1799086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3e72035a49ab8d5bc06e41b294525e4ecd6e5e98","datavalue":{"value":{"amount":"+0.7320381999015808","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":"Q2164244$CED1AEE8-D169-486D-9325-65CDB3C92D1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"634865f6354839c52530abb008d3913b47aec7f9","datavalue":{"value":{"entity-type":"item","numeric-id":2152274,"id":"Q2152274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"70e69208236ed7138b2615fb72566ec29c861081","datavalue":{"value":{"amount":"+0.7250365018844604","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":"Q2164244$653FAD90-5AC2-4948-BFBF-E9CBD71E1C94","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":"76cc4e5f1e466a8fc261da32d3b991a85e7617da","datavalue":{"value":{"amount":"+0.703478991985321","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":"Q2164244$CCD35928-2078-48E5-92FA-0E6949C97AC0","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2164244","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2164244"}}}}}