{"entities":{"Q2703760":{"pageid":2714505,"ns":120,"title":"Item:Q2703760","lastrevid":82756223,"modified":"2026-05-06T21:52:41Z","type":"item","id":"Q2703760","labels":{"en":{"language":"en","value":"Using theory interpretation to mechanise the reals in a theorem prover"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1576685"}},"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":"Q2703760$DD2E0C2E-A7C5-4807-B71D-19F9480C6468","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"84aa1f814dc1c835f8f1eb3b44050d9d3720e121","datavalue":{"value":"0970.68146","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2703760$C1D75883-3F90-4014-B278-33BBFFAE484E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"2a52892d10a4029816f3d3c494a0c2b4804837c6","datavalue":{"value":{"entity-type":"item","numeric-id":2703758,"id":"Q2703758"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2703760$C64E3536-A8CB-41FB-91E8-609962D67117","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ffdb1dd75cd4312e715709efb5cc8beb218a80dc","datavalue":{"value":{"entity-type":"item","numeric-id":172105,"id":"Q172105"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2703760$612204F1-2129-4862-B089-0EACCBAAB086","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e64df37aebf538545e6964f8427f1f79eb627784","datavalue":{"value":{"entity-type":"item","numeric-id":2703759,"id":"Q2703759"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2703760$D38768D5-E128-4E3D-813D-D756AD98F069","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ea2ded88325e903b7f55f9d8e847a5de315d1740","datavalue":{"value":{"time":"+2001-05-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2703760$8FEDCBC6-9187-40A2-B603-23FEB9FAF08A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2703760$751D9F29-C624-42A1-BCF1-4C61EA0AEB8E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2516e7d521d40d3cf3042046e14385155f9e0aaa","datavalue":{"value":"1576685","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2703760$6CCD2FC9-6647-4335-A29E-B4D2CA700743","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dbc0f5fa3d1c04210a7b2d99a12d6bfe1435e6a4","datavalue":{"value":"theorem power","type":"string"},"datatype":"string"},"type":"statement","id":"Q2703760$63FE33DA-747A-4B80-9225-8928F0D47F0E","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2d75f286d3b7fafc7959ecf913797da4cf0ecbd8","datavalue":{"value":{"entity-type":"item","numeric-id":30419,"id":"Q30419"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2703760$2E370DC4-3B68-4CA5-8349-01D6CB636CCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"59de9499168d91da1b1ff36408be93f573928689","datavalue":{"value":{"entity-type":"item","numeric-id":30420,"id":"Q30420"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2703760$A3803659-7EA4-45B8-A820-945D6605F62A","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":"Q2703760$81C183B8-D01F-401F-BDF2-C12FAB03D0F7","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e87769249be4f419bd31557379ee5381ae8453d6","datavalue":{"value":{"entity-type":"item","numeric-id":1015381,"id":"Q1015381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d2b30f5605cee2d1282e9b0db87c4292a2aa1508","datavalue":{"value":{"amount":"+0.8989467","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2703760$16E110D9-D8A7-480C-AC41-4E4DA4CBB7D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a8bfe1579abd1aa529055d84308768a923e2bf5d","datavalue":{"value":{"entity-type":"item","numeric-id":2754041,"id":"Q2754041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fcde2dd65e78e8c3266f2726eb7fc8b3aba3f03f","datavalue":{"value":{"amount":"+0.8830925","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2703760$E25C0A18-2957-4213-8B54-8C2E2A3500E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"15ccd8d62bc07eeb7dc47fcb777194d3ff4f05e1","datavalue":{"value":{"entity-type":"item","numeric-id":4681810,"id":"Q4681810"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"04be8407beb8f35733a871cfd766391794c3e12b","datavalue":{"value":{"amount":"+0.8757439","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2703760$4961D858-3B96-4303-88EF-C72FE5CACC00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ff9ddc6fe1a55941c90677f589ce0b4da36c7df","datavalue":{"value":{"entity-type":"item","numeric-id":4944901,"id":"Q4944901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9c2b4003e3661a66c62ee36d515d433ba703fb90","datavalue":{"value":{"amount":"+0.869195","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2703760$0221FF7D-E11F-4880-8581-C2E2B812BF6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"72211653300131d81cff354d1410fa3cdbd7ded0","datavalue":{"value":{"entity-type":"item","numeric-id":3726110,"id":"Q3726110"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"27932fb13ffdb66edaa80581eee2ef685f990f9b","datavalue":{"value":{"amount":"+0.8641119","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2703760$C9A36643-7C81-462A-B17C-FD12BBD126E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"da37791c9e2e732ecd85d3ecc7996e5b3bfc227e","datavalue":{"value":{"entity-type":"item","numeric-id":3003309,"id":"Q3003309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c8441ac69274f79c085457b46c12bcd6a95d7383","datavalue":{"value":{"amount":"+0.8628125","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2703760$55D61647-DF22-4A2B-B721-FD0CBAB5A70D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d97cb94e392302237f2f3a394c50c071b2af711c","datavalue":{"value":{"entity-type":"item","numeric-id":3644745,"id":"Q3644745"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f55f4d32cda5d6cb1c17a3048355342d1d838b6a","datavalue":{"value":{"amount":"+0.8613157","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2703760$55059882-0CE2-4528-AA9E-85695DE86D2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"baf36049823cf0a0132e9179cb0e74e04f41c978","datavalue":{"value":{"entity-type":"item","numeric-id":5394621,"id":"Q5394621"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ab15a659f92ca3c40f3d21deb04f45bc5f7f76ad","datavalue":{"value":{"amount":"+0.8586126","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2703760$C59F1C32-0050-4A76-8D7C-F6BFE96B2EDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e15ab56d2932edec5b9ee12d91469df76fa2fb0b","datavalue":{"value":{"entity-type":"item","numeric-id":5505488,"id":"Q5505488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e9821de2ed768f503aed2a38d23230bbac7dd3d3","datavalue":{"value":{"amount":"+0.85608965","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2703760$BDF2CCE8-3415-4AEA-A466-A709E9A2B92D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bd7be6caaaa2c317c345966210e02cb9b65737f9","datavalue":{"value":{"entity-type":"item","numeric-id":2973239,"id":"Q2973239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"778361efc2f82467f0ad61b69c41522a1a2045f6","datavalue":{"value":{"amount":"+0.85579","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2703760$46B105FB-E0D3-4E9E-9C4E-C444F778CC3C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8f15b1dbb8281bdb3173730ca335ff21f60008d3","datavalue":{"value":{"text":"Using theory interpretation to mechanise the reals in a theorem prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2703760$A1A096CF-E612-4F51-B734-B77B9408F2A6","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Using theory interpretation to mechanise the reals in a theorem prover","badges":[]}}}}}