{"entities":{"Q1799078":{"pageid":1809820,"ns":120,"title":"Item:Q1799078","lastrevid":68987130,"modified":"2026-04-13T03:33:28Z","type":"item","id":"Q1799078","labels":{"en":{"language":"en","value":"A Why3 framework for reflection proofs and its application to GMP's algorithms"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6958099"}},"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":"Q1799078$721BCF68-ACC7-41AE-AF2B-001FBFFB3121","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e63f97efeed29bd874f8cd903ce9a5eda50457a8","datavalue":{"value":{"text":"A Why3 framework for reflection proofs and its application to GMP's algorithms","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1799078$DAD9D73C-9F2F-4D54-BF9F-497A2FF567BA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4a409575d6e2f327f6d05c0ad5490e89440c5b57","datavalue":{"value":"10.1007/978-3-319-94205-6_13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799078$7FCB657B-0B04-48D7-8FBB-349B71ECF8CF","rank":"normal"}],"P16":[{"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":"Q1799078$804F0EC6-8AA8-4514-AF0E-2471970209E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"075558066d8466e014452f3e65237d2978788c6f","datavalue":{"value":{"entity-type":"item","numeric-id":1630030,"id":"Q1630030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799078$4F94A4B9-FA20-4CB0-A21E-2BF00FAA0F26","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0172cdede3f306f1b36155a82f67164814fd11e5","datavalue":{"value":{"time":"+2018-10-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1799078$67F0DA7D-8256-46ED-97A3-2AEB5D3D102B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8d8867a13a1f015ec016b6acbfa2e5e85b209251","datavalue":{"value":"https://hal.inria.fr/hal-01699754v2/file/main.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q1799078$06C1B526-BBCC-49E0-BD86-4A751A90F2F8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799078$1658F61B-E5E0-43BB-9315-5FDBFFDB1E3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799078$D45BF77F-8C12-4785-BFBE-3181D6ABE303","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"50208b9ac562fa89f715ec5ec86c817b580324ef","datavalue":{"value":"6958099","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799078$34386C9A-B369-4A48-A282-E1962931D39C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dfd2ae52b3325778b0c72742b08c947a3c4a2c65","datavalue":{"value":"decision procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q1799078$D217C8D8-ABF3-4E8A-B4D0-E69D7AFF3A6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"54d1cab2e3b73c7e67539d9d2affca1e56a23d54","datavalue":{"value":"proofs by reflection","type":"string"},"datatype":"string"},"type":"statement","id":"Q1799078$926A927A-4317-480B-A308-57A5DE6B481B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"757d965346c06c3204f84840816c70899ad83131","datavalue":{"value":"deductive program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1799078$5C3F025D-271A-4395-B2A7-521593C83BC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"713b3edb20b5ecd22e3c8a9a008ea9eeb475031a","datavalue":{"value":"nonlinear integer arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1799078$AAD4220D-71E4-494A-B001-166A92BC5F60","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b6da1f42e3d4d28e24ecb68672c28ee0982a60c2","datavalue":{"value":{"entity-type":"item","numeric-id":12950,"id":"Q12950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799078$C28FAD95-7BDB-458A-B676-B3264911E8DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"602b32d79a3dd12c7713e80fb0597b8ab4375f08","datavalue":{"value":{"entity-type":"item","numeric-id":16614,"id":"Q16614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799078$854F4197-2C26-41DB-A33F-3463B45E8D41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"94a83aebbff287adfc2566cf5a58d543fa9638cc","datavalue":{"value":{"entity-type":"item","numeric-id":21152,"id":"Q21152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799078$63462095-4991-44AE-9A84-9CC7AD20A058","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d4f20857e79be9881c5d7a06583454f1cf2611e9","datavalue":{"value":{"entity-type":"item","numeric-id":24994,"id":"Q24994"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799078$1FD80755-B4F5-4A90-824F-CBFB56D802E8","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":"Q1799078$B599558D-4D61-4B8F-B28E-E8F6283283BA","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b2c58e806a1bc4190fced7ea83f3a113ec325590","datavalue":{"value":"W2786891599","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799078$AEB92FBD-DF3B-4F5D-9E17-625AA9345D1B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"55cfa683e4e84d4df63e52e97fea2c13bca6a792","datavalue":{"value":{"entity-type":"item","numeric-id":5130751,"id":"Q5130751"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d6e3fecf11a71ba7d0deb7c0ad6f8bdbd919c4b6","datavalue":{"value":{"amount":"+0.784069299697876","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":"Q1799078$2ABAC279-D6C1-45A6-921E-B84203BCBCDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1a5b6de0488af39ef3830498792881213aa4e86d","datavalue":{"value":{"entity-type":"item","numeric-id":2938045,"id":"Q2938045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b1327b102ed5b8ca1d2c09f1ab442a019bcb8644","datavalue":{"value":{"amount":"+0.7334491610527039","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":"Q1799078$8DCB3EA5-82C1-46A8-AFB2-66B312E5E6CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a9c2bbb3df2b96668f129f74b95b0e10b1d032e5","datavalue":{"value":{"entity-type":"item","numeric-id":5326280,"id":"Q5326280"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b144846ef557a863bec1ad0b9ba441fa3a2c4598","datavalue":{"value":{"amount":"+0.7265649437904358","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":"Q1799078$B658808B-D253-42EF-B88B-E05F2D5C60B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bc100a827024adf359968eefa34f376fa6d61656","datavalue":{"value":{"entity-type":"item","numeric-id":1703015,"id":"Q1703015"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2bf9bae84cd965aaf1c87dfc571ffcbd53ffcd54","datavalue":{"value":{"amount":"+0.7154501080513","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":"Q1799078$84878607-3AD4-4EC9-9484-15123FB208E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"435c230f2e936567467c911556c7b07e730f6c8f","datavalue":{"value":{"entity-type":"item","numeric-id":2802496,"id":"Q2802496"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f7447735cdf89dc6bc872a2d06e0a2862b23b63b","datavalue":{"value":{"amount":"+0.6876853108406067","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":"Q1799078$7F26745B-5BCA-44E9-A2D8-B8FEB49A0EDB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A Why3 framework for reflection proofs and its application to GMP's algorithms","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_Why3_framework_for_reflection_proofs_and_its_application_to_GMP%27s_algorithms"}}}}}