{"entities":{"Q6136749":{"pageid":13271056,"ns":120,"title":"Item:Q6136749","lastrevid":47890639,"modified":"2026-01-03T00:11:37Z","type":"item","id":"Q6136749","labels":{"en":{"language":"en","value":"Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7732883"}},"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":"Q6136749$E36000F8-EFB4-4498-B277-5E2C9F776DA2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"953b9e9111da1909625915365f7868326c8f5d13","datavalue":{"value":{"text":"Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6136749$FE3D4C8A-39A6-4746-B9C0-EDBE9B756D9C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9ddd006acbf45d3f5ad1bff6b5b2c5ec4985f6ce","datavalue":{"value":"1522.68306","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6136749$BAC1CAD2-EDC2-4DA4-9659-E747EF4E9143","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ed28fda67265d55c0759179f9646488f7dc07e66","datavalue":{"value":"10.1145/3543670","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6136749$A4AC0294-DCAC-4649-91BA-D2FEB6723781","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"bb5994611d51d77ee41c5e35bedc55b9725823b7","datavalue":{"value":{"entity-type":"item","numeric-id":6136747,"id":"Q6136747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6136749$FB10980A-BBA4-4AD0-8A59-48E8A0258D45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cb5dfbdfa6d8a2070a67ff948fb8abd387eda36e","datavalue":{"value":{"entity-type":"item","numeric-id":352969,"id":"Q352969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6136749$BEFCF8BE-209F-46C9-BE0D-C061E20DDA9C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fe3ab95714c2c404c41c322f490837563b2323dd","datavalue":{"value":{"entity-type":"item","numeric-id":5267392,"id":"Q5267392"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6136749$BDBA65E9-3B0A-452F-8C97-F30C6A0B3C27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9374537cb528ae7c9ec4f27f17812fe662671906","datavalue":{"value":{"entity-type":"item","numeric-id":6136748,"id":"Q6136748"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6136749$D7155D5E-2B23-4807-9FEB-1D4069DBF84A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d9925518446645d219093152a820aba790417b61","datavalue":{"value":{"entity-type":"item","numeric-id":164203,"id":"Q164203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6136749$485DE407-8938-497F-A252-5B806225E969","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"8ed1b97c874aa96cebcf9bd9f2d490f4bcf42073","datavalue":{"value":{"time":"+2023-08-31T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6136749$00A9C8F8-52E4-48D9-8964-DEC1B7F1E6B6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6136749$E4EB2A97-5AED-4231-B033-127FBA872E8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6136749$982B86C2-6666-4ABE-A61E-436FF2944B5A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"60e0d7490e11377f053184c0092b2bff78cbf9ad","datavalue":{"value":"7732883","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6136749$7AACFE0E-5208-402B-B00A-C2F2DA246C08","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8bf549142b710f01581b24fd28cbb67614316cd4","datavalue":{"value":"theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q6136749$F2DE324E-866D-4F08-ACA7-E6FB1560CA11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"819f137f9ec626acba1c8947981be8a93c7821b2","datavalue":{"value":"transcendental functions","type":"string"},"datatype":"string"},"type":"statement","id":"Q6136749$A218FF00-E4C5-42E5-ADD2-799F68F7FAC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ee875072f43e1c3512cce0e7890884571a676d22","datavalue":{"value":"floating-point algorithms","type":"string"},"datatype":"string"},"type":"statement","id":"Q6136749$B7E5870F-8AF6-4382-B2DB-256A81BF02CF","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":"Q6136749$7DDE794A-30AA-4D3B-9F2C-5620430DF226","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f1e3dee0f560de98ccfec423e540b97246eeeab0","datavalue":{"value":"https://doi.org/10.1145/3543670","type":"string"},"datatype":"url"},"type":"statement","id":"Q6136749$E3D2CC88-AEF8-4DC7-BF70-013D52998425","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"76a524b947f72a42961bdf933f4b1ef852598e21","datavalue":{"value":"W4282832561","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6136749$0018FA32-03AD-4E96-A810-E0FD77D60807","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"843c4414d953c2872263c04a833c3fb6dd1fcb3b","datavalue":{"value":"Q113769892","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6136749$FD0F6CB0-729E-4663-87BA-C0F54F61ED7A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"13e649264ee8c5f77323097969c0d9813410c2c8","datavalue":{"value":{"entity-type":"item","numeric-id":2754046,"id":"Q2754046"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"15d5881f38c1a7d6d85c70247044dfb1f5564791","datavalue":{"value":{"amount":"+0.7714260816574097","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":"Q6136749$B09B4ACF-916F-4EB5-B995-AD9297A327BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4ab5af0b01032fe41b463bb1909a4831e2c66566","datavalue":{"value":{"entity-type":"item","numeric-id":816201,"id":"Q816201"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d0c06018771b481cd323c6db1f976c6e436bec83","datavalue":{"value":{"amount":"+0.7598647475242615","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":"Q6136749$25C70CC6-8273-4E7F-B4CC-7FC37A8A7B71","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":"447496d89bfb3ae3c0b352845a642567b31bfffd","datavalue":{"value":{"amount":"+0.751075029373169","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":"Q6136749$E852ED10-A4D7-46EA-97D5-645AD54F05DA","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":"58c03df1b9f76f123e8a402d4f3d7f3088c57f84","datavalue":{"value":{"amount":"+0.7509987354278564","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":"Q6136749$17648234-2053-4831-B6DE-70516A944A2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"764c246a1e922833020056c629835fdd29caec98","datavalue":{"value":{"entity-type":"item","numeric-id":5492965,"id":"Q5492965"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"530ec2b5b752215b25becca35fedcb237150f2ce","datavalue":{"value":{"amount":"+0.7462198734283447","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":"Q6136749$F5A82F7E-AB5F-4B3C-968E-0ADA6FD0E9BD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6136749","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6136749"}}}}}