{"entities":{"Q6053846":{"pageid":13188001,"ns":120,"title":"Item:Q6053846","lastrevid":39672969,"modified":"2024-12-30T17:01:30Z","type":"item","id":"Q6053846","labels":{"en":{"language":"en","value":"Enabling floating-point arithmetic in the Coq proof assistant"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7753652"}},"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":"Q6053846$DE36EEFC-E336-4C9A-A70A-F56C6F6CA974","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"bff86d9f24854568229cb7b1bad43db2d5c403a1","datavalue":{"value":{"text":"Enabling floating-point arithmetic in the Coq proof assistant","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6053846$80D3B3DC-11A1-40FB-A2D5-2BD2116F6916","rank":"normal"}],"P16":[{"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":"Q6053846$7B5782EB-EB85-4E2B-8895-4DFF293DF83D","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":"Q6053846$889FC6DE-E4C1-43C9-8D9A-D529073ABBFD","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":"Q6053846$986F0A4E-082A-463B-8BB3-E239678EAFFF","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6053846$B0BB66BE-1110-411A-85E7-1432395A36CA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"cc38c107bfbe3d21f38c865385857570a4bd451a","datavalue":{"value":{"time":"+2023-10-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6053846$A5595B13-05D1-4F78-90AB-526DB17E6071","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6053846$0A53078F-4B7E-4B2A-90AA-375BF54CF234","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"82980589fbca3d22854054e227f9e7bd26f811a7","datavalue":{"value":"7753652","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6053846$C78AB849-AEAC-401E-82CB-0D6DDD4DA06F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"326c300cf62efa849a7bdb94dd90663d744d9f5d","datavalue":{"value":"formal proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q6053846$956C96C7-4EB7-4D7A-A203-CF2ED5B12031","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"00216556e27ad3bbc2d642874d0693b52d5f53d1","datavalue":{"value":"floating-point arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q6053846$1E6439BC-59C5-4218-9C83-127ED953458A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0c2644d758febee2db7e76a373455c01029edf33","datavalue":{"value":"proof by computation","type":"string"},"datatype":"string"},"type":"statement","id":"Q6053846$56C7E112-C219-4A92-BF3A-B997A6DC6473","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":"Q6053846$272869C4-5D50-4D91-86BF-E3DCB71FCA0A","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":"Q6053846$78258FD2-748D-45BC-BA48-8BB80324CA99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16d69daa34c11e7542755ef35435ce2320824878","datavalue":{"value":{"entity-type":"item","numeric-id":5875413,"id":"Q5875413"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6053846$E99FC086-CD41-4A18-954E-F8B7BF9F7D0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6088134b435dad2c73dd6160b51b58bfb3122a79","datavalue":{"value":{"entity-type":"item","numeric-id":2352505,"id":"Q2352505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6053846$B5AF94D0-A74F-46C4-AE69-5FF77EE5870D","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":"Q6053846$B517C195-1485-40B9-90D5-13FDFD659E5B","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":"Q6053846$887B082C-973B-430D-B3C1-D518B7B70FF1","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":"Q6053846$19A1C992-6B3C-4A24-A3BB-CB8A29E2696D","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":"Q6053846$EEB8BF02-586A-4AC1-94B5-300BEA801545","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":"Q6053846$E7B341C6-196C-4599-A11A-0B2DDB78935F","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":"Q6053846$57A6E1BF-55B5-49E6-8D95-FAD35CFBA1AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"188db94fd9c26525c0ae702cb56edad629ab92ca","datavalue":{"value":{"entity-type":"item","numeric-id":4609588,"id":"Q4609588"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6053846$6E80317A-67DC-4168-B577-8217A55C12BD","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":"Q6053846$E17F3934-0839-4CF5-8EF1-21DBA5C0133A","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":"Q6053846$B6A3AA7F-CA68-4819-8C37-87E0A0A8612C","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":"Q6053846$CAFEF6F3-0D09-43EA-861A-6178A8E1048F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"55571c266c2febc0928afc543a0e3d875de4d007","datavalue":{"value":{"entity-type":"item","numeric-id":1601363,"id":"Q1601363"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6053846$5539E535-8EAF-4745-B822-11E2119A2BA5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"45c0f970282b6476c842f62135ea681b390c1139","datavalue":{"value":"10.1007/S10817-023-09679-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6053846$51D5A82B-46F4-47FF-A0C3-7B7BF90DF13F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6053846","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6053846"}}}}}