{"entities":{"Q5875413":{"pageid":7904964,"ns":120,"title":"Item:Q5875413","lastrevid":39654617,"modified":"2024-12-30T16:43:26Z","type":"item","id":"Q5875413","labels":{"en":{"language":"en","value":"Primitive Floats in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7649956"}},"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":"Q5875413$4E255D49-044D-4EA9-851E-BECBB416249F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9bc2a4bdc957baba8d8db21f4b64d2e610b012ac","datavalue":{"value":{"entity-type":"item","numeric-id":5875412,"id":"Q5875412"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$90C1BDDD-0D21-42FC-84CD-BB59517E22E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"232dbbf2f85a77956592acb3d7bdc0a70d26a60f","datavalue":{"value":{"entity-type":"item","numeric-id":331613,"id":"Q331613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$DAB26041-22AA-498C-9002-B2C2798DD200","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f5979152cca5de810ef5e74808ba838cbede6b12","datavalue":{"value":{"entity-type":"item","numeric-id":888468,"id":"Q888468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$1D2A3EBB-518B-4582-97B3-5E79FC042825","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6695abe38664d65c38747de7b5fe54d9caa92dea","datavalue":{"value":{"time":"+2023-02-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5875413$7BB3659B-D9E2-4C3C-A7D5-C35B55B5B2B2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875413$2809595E-F97A-4E09-AABD-6BE12373E7B7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"474cf6a379b7f0cad3403c3fb397c90af7e56377","datavalue":{"value":"7649956","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875413$D7D2B836-4FBE-4D30-B061-F1821706D053","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6ee02fc9bd52bc41c092cce9d88ab018ecc2a148","datavalue":{"value":"Coq formal proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875413$5F263C8E-D097-4EA9-A989-9A09805516F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"00216556e27ad3bbc2d642874d0693b52d5f53d1","datavalue":{"value":"floating-point arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875413$5D3A676B-8E8C-46D1-BA87-6FB8A690E2B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ff739b6ae75a81f8c57050f70fe3c1c8c007c273","datavalue":{"value":"reflexive tactics","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875413$499C12B8-2995-485F-B041-10884944E6B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ed2d4f54838e863aafaa1049719054384eaf08b","datavalue":{"value":"Cholesky decomposition","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875413$37B2ABA3-2275-49F0-8AA0-E059184EC2B9","rank":"normal"}],"P1463":[{"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":"Q5875413$3D311090-8E6A-4B35-B7C0-19A74B304A54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"31d2ddeef485fccfd3a5fe32ea329d2b65b4f1b4","datavalue":{"value":{"entity-type":"item","numeric-id":35396,"id":"Q35396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$8883BC84-90F2-46E7-82FF-A5A77A2546D9","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":"Q5875413$71C45FBB-0AFC-4813-8FD1-C4ADC5D83EAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"76ddbdc03eaf78993a82a2e5c6c59ab61f4d3d1d","datavalue":{"value":{"entity-type":"item","numeric-id":29941,"id":"Q29941"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$CF0DD69C-AEB5-43DC-B092-33742FF35F49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9bbedeb8fff9bf5dbcadd59c3f5332134c82fe9a","datavalue":{"value":{"entity-type":"item","numeric-id":16987,"id":"Q16987"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$91B5D874-BBE4-4E66-8D9C-C1DF96D489F3","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":"Q5875413$F78F8DDE-71B4-4718-9B45-134E3D70CBF5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"48a15f52ce1f00b6ba364b5cb457dea2e7101aec","datavalue":{"value":"https://hal.archives-ouvertes.fr/hal-02449191","type":"string"},"datatype":"url"},"type":"statement","id":"Q5875413$2552405E-0A95-4D78-833D-763A2719ECC0","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6f6c1f0dde40c8f35a32c2b55e426b78626beafd","datavalue":{"value":"W2981852708","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875413$8C3CDF67-DDC9-4285-BB86-3A683920899C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a4c73ed1bd47ca8f13af784d9daf1113fff32b76","datavalue":{"value":{"text":"Primitive Floats in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5875413$E18D4B15-FFC8-47FD-87EC-5DA8A6940205","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f788536331bb87ba4e75963340b885a6c5e47c5c","datavalue":{"value":{"entity-type":"item","numeric-id":5747643,"id":"Q5747643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$07917054-FD8D-43AA-A71F-977255E7F9F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"076a838bd0092606d2a19431691467a449edab0b","datavalue":{"value":{"entity-type":"item","numeric-id":2751370,"id":"Q2751370"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$70B140F3-6238-4061-B7C3-B12CD734ECE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ab1fb3b741de6ad15a6cf3e725ed00bb86921b6","datavalue":{"value":{"entity-type":"item","numeric-id":5274886,"id":"Q5274886"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$DC007EAF-999C-4169-B9E1-899AEC3BE471","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f41449a4ec7451f64a128da49483496b397b48a1","datavalue":{"value":{"entity-type":"item","numeric-id":2938045,"id":"Q2938045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$2DC62ACA-9F96-442E-8516-7E7145C0C4E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"99e10366aa14b4f4cc11a9a253b0c3ce76fb85ca","datavalue":{"value":{"entity-type":"item","numeric-id":2549229,"id":"Q2549229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$284A27C8-3EAD-4A25-8E9C-EC3506886779","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58b61ff436ad097e7899027abdd6e0c42fca0ee2","datavalue":{"value":{"entity-type":"item","numeric-id":2164216,"id":"Q2164216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$9080D164-4988-4F26-86A0-5543CCFE730C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7d9190693f3924b86be7203c014f0b8b161bc6f8","datavalue":{"value":{"entity-type":"item","numeric-id":5302559,"id":"Q5302559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$769B75ED-B6A3-4F57-ABCC-48AE1BDA375F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"901ba45472e1a0a3be8b2e40215973355027ef09","datavalue":{"value":{"entity-type":"item","numeric-id":2949209,"id":"Q2949209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$367A64F8-5977-43FF-ACC5-7AC3914D86B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c6f7860107870a9dd8ca3afddc064363fcd28a79","datavalue":{"value":{"entity-type":"item","numeric-id":3613425,"id":"Q3613425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$E1B5D559-9ECA-4152-A21A-FCF25ADFAB21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb4857d0d243b746647a153e1690cd4acc84f69e","datavalue":{"value":{"entity-type":"item","numeric-id":5280247,"id":"Q5280247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$B2D8B06C-DB44-45B0-BFB4-11788F68EA27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a83e6b1f38bd22e7c559f56363b9c482c696cc45","datavalue":{"value":{"entity-type":"item","numeric-id":4864704,"id":"Q4864704"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$07F20AB7-4DF0-4156-8DCC-58A0E5649533","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77c9d5a575b9e1cb1a369c580951e34943f4cf11","datavalue":{"value":{"entity-type":"item","numeric-id":4600709,"id":"Q4600709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$E62956D1-FD52-473B-8F2E-424BA761F7C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ff81489e80366438468bf6dfe10c7a159bc3ea8c","datavalue":{"value":{"entity-type":"item","numeric-id":4057549,"id":"Q4057549"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$8E04B8E7-94AB-4200-82EF-E7FFF554029C","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":"Q5875413$5577AF6C-D08A-4687-BD18-E5FD61089625","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c18f6d1d44ef740fcb363b3e7b055f66c3e3376b","datavalue":{"value":{"entity-type":"item","numeric-id":1791180,"id":"Q1791180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$55312BB5-4999-4728-B69E-CD9CD05658F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d9b953e3a38cb9987d56770768dcde6df4c409e2","datavalue":{"value":{"entity-type":"item","numeric-id":5195260,"id":"Q5195260"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$A0E5B063-0C57-4D88-8DC7-492536C52D85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe5e921e331154ac4053c6ddf9609e27a78717d8","datavalue":{"value":{"entity-type":"item","numeric-id":331615,"id":"Q331615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$5977F03D-0E06-45BF-A0F5-14B9EB9E3AB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98138980df53423c6ebdb27048e3d572db23b08f","datavalue":{"value":{"entity-type":"item","numeric-id":5339762,"id":"Q5339762"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$0DD9F9B2-E1AD-4258-8004-3B884E3D52CA","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":"Q5875413$2660FC96-295D-439A-8A95-D9547886F78A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0125d89375f687135d25dadc26674dd9692fc0d4","datavalue":{"value":{"entity-type":"item","numeric-id":2013318,"id":"Q2013318"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$E6C8A0A9-48F4-4552-8503-5B161627BAF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dcf15b8407e5d75aba6434845813c7baa49e06b2","datavalue":{"value":{"entity-type":"item","numeric-id":2502318,"id":"Q2502318"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$68E4BC0A-5A68-45B0-81F8-B08874A2A933","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"758d3724017c484fb2035201d7ba18e8ef7868f8","datavalue":{"value":{"entity-type":"item","numeric-id":2890535,"id":"Q2890535"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$DD3871EB-EADB-4033-9F5C-F4A590129F30","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":"Q5875413$CDBABE6F-45B5-4A02-9A6A-01AF0E2A16BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d0f8e5d721127fb6a9eff1f4701a2abac8da5592","datavalue":{"value":{"entity-type":"item","numeric-id":2391021,"id":"Q2391021"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875413$135D3159-5AB2-4713-8844-35B3C7CD61F5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e3e0f802e63f89d745f203b5b2c2e99eaff591f2","datavalue":{"value":"10.4230/LIPICS.ITP.2019.7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875413$3F752C8E-7B35-4F97-8183-270F35632683","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5875413","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5875413"}}}}}