{"entities":{"Q3543660":{"pageid":5573564,"ns":120,"title":"Item:Q3543660","lastrevid":50516543,"modified":"2026-01-14T06:35:02Z","type":"item","id":"Q3543660","labels":{"en":{"language":"en","value":"Real Number Calculations and Theorem Proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5378183"}},"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":"Q3543660$AF6F62DB-7648-4780-82A2-A5187E2DFDB9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ae10fe80d1b78d993a52a7046c7e75026131e725","datavalue":{"value":{"text":"Real Number Calculations and Theorem Proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3543660$6326B3D0-88B8-4D50-9611-233D7D5FE80B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3733f4fee10d31e729bd602634bff052beb6ac11","datavalue":{"value":"1165.68463","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3543660$CC67A668-FE47-439D-A2A8-6500C1262434","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8aaba38b97753d7b2583f3ede00037832cb0944c","datavalue":{"value":"10.1007/978-3-540-71067-7_19","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3543660$D2E9AFC9-2993-4022-A803-0327CD810D5F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7191134f319418d58727fd4a71fc323f51bc3b02","datavalue":{"value":{"entity-type":"item","numeric-id":714619,"id":"Q714619"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543660$60E178BA-50B3-4AE0-A8CA-0C2ED8A33AEF","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543660$1628ABE4-1276-44C7-9299-6D4BAAB56DB8","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9390341f6bd0adb4a80933997da5182af87828a8","datavalue":{"value":{"time":"+2008-12-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3543660$CDD46BAE-3EB6-441C-898C-B541D948F7DC","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3543660$B4A161A2-82B6-47C1-B3C6-4BFE5503760B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"74066a906c5dfce47176a47252f0d30605d710c7","datavalue":{"value":"5378183","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3543660$C836361D-0F63-4EC4-96B0-1EC1317F2F9C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6a750407036b37c9b3abd18e15b0b3c77ba88a22","datavalue":{"value":"computable reals","type":"string"},"datatype":"string"},"type":"statement","id":"Q3543660$A812E0B4-E526-47EB-8A2B-6062D6913402","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a94e026fd02207d3e12582b589793dd778d12a8d","datavalue":{"value":"exact arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q3543660$C3B11CBA-D795-4546-A2FA-8C7C0D0FE9C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q3543660$B8A8BE26-7D81-4913-9AEB-7BB031C40CB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b3d3d0d2409011411be91984a4137a1c90ca04ff","datavalue":{"value":"PVS","type":"string"},"datatype":"string"},"type":"statement","id":"Q3543660$69019229-D963-4382-A511-B8FEC2360D85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q3543660$6118C58E-E4BB-4E77-8F80-03373309BBF7","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543660$9092A7B1-4CDB-4A65-9813-5C9101640644","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543660$9AB8E3AE-1F95-44E6-B89B-059C847CCB0E","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":"Q3543660$7626362B-25A9-4750-B5D2-0943F2AEB652","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f5e84ef89f8695e539a6e75b1505be39b1ce51a0","datavalue":{"value":"https://doi.org/10.1007/978-3-540-71067-7_19","type":"string"},"datatype":"url"},"type":"statement","id":"Q3543660$1DA3C57E-884E-42B6-929E-0A7459B58C7D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a1a9f93c48132bc762eb8f33c58af9845953abc1","datavalue":{"value":"W1586880486","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3543660$0773B76F-8580-4A21-AF24-C1A360EE025F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b7be2d05c20413feb6443e1b1af122bfdc77cfe","datavalue":{"value":{"entity-type":"item","numeric-id":3498456,"id":"Q3498456"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543660$AFD74629-E643-4054-B9B1-F9781CF9627E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a02ebf0568f47635f182c488d881f7744ddea83e","datavalue":{"value":{"entity-type":"item","numeric-id":3803111,"id":"Q3803111"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543660$395ED0D7-AE9F-47E3-8A58-748B642D09D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7775af0dfcf78f0eb01b93b06a122479305aedfd","datavalue":{"value":{"entity-type":"item","numeric-id":3431543,"id":"Q3431543"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543660$C7114D9A-0D63-4810-9BAC-911F1B2CCACF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7292935a36dc885e30d50eafb37d17a292338c33","datavalue":{"value":{"entity-type":"item","numeric-id":3922157,"id":"Q3922157"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543660$F0771030-2EAB-4CF8-8B43-3C655D5DB85B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f64715e3d5e62c01018eba7714ed518e14c6fbe3","datavalue":{"value":{"entity-type":"item","numeric-id":3226752,"id":"Q3226752"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543660$DF05B161-811E-43F0-BB78-78964CEA8251","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4835fa2e4d7885449ed59928dc6f8b9b1ef0d39b","datavalue":{"value":{"entity-type":"item","numeric-id":3227569,"id":"Q3227569"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543660$A6EDE2BD-CA25-44BD-BFE9-8A59CC4B5ADD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"be3d8fb3ea0608a30440ec139e9f2dbb425b2918","datavalue":{"value":{"entity-type":"item","numeric-id":3244109,"id":"Q3244109"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543660$5D9E67A2-4963-431B-8664-D6F6E9464013","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da5c4c6269cfab8e5917ddd21b6126adfe8f1934","datavalue":{"value":{"entity-type":"item","numeric-id":5458427,"id":"Q5458427"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543660$5B6E76FE-E613-4573-8C1F-02920F4F1BAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"584c7a9a835c28d4ba3d73747c45581adc6618fd","datavalue":{"value":{"entity-type":"item","numeric-id":5308359,"id":"Q5308359"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543660$343A96B2-BAAE-471B-9050-84DD70A4C4C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9bbafb4c632b6a6b9de7527d8aee97aca0cf6440","datavalue":{"value":{"entity-type":"item","numeric-id":1853641,"id":"Q1853641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543660$745C1A5A-0C2C-4684-8A82-6E376F0139BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"552c0fd0688cc1cd0d242c6ea1573c9e5fd80831","datavalue":{"value":{"entity-type":"item","numeric-id":5477656,"id":"Q5477656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543660$768C38E9-31F8-4D2E-A185-A8070F47369B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a10bbeb6c6903ace983b2dbf286a2ef4e5b248ab","datavalue":{"value":{"entity-type":"item","numeric-id":1331625,"id":"Q1331625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543660$2E95005C-3130-4AEF-B10D-AC8420145865","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"def2c931176027a2e91972d8f217f89dea0b484e","datavalue":{"value":{"entity-type":"item","numeric-id":3994907,"id":"Q3994907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543660$88F14FC6-A635-4B21-A1C1-EFAEB86F253E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1613a6ff5ac7b010de5ba58e55ebd9cdec3d5273","datavalue":{"value":{"entity-type":"item","numeric-id":5765445,"id":"Q5765445"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543660$D9E79039-FE3A-422E-878B-96B152C881DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eba8934df744678f296d65df2505ca4669717fde","datavalue":{"value":{"entity-type":"item","numeric-id":5768086,"id":"Q5768086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543660$08958718-7D79-416D-B32C-5EC738206672","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"11bdae9f731c0e1145ebd1c0e2604117a0993d0f","datavalue":{"value":{"entity-type":"item","numeric-id":5477656,"id":"Q5477656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fd8095ae619c66cf5e430564184cb6592382e916","datavalue":{"value":{"amount":"+0.8515880703926086","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":"Q3543660$3AC50E09-7B0A-4414-9C33-6338C864B4D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"470f9f7684c1dfc5eb04bac92aa78095ad543232","datavalue":{"value":{"entity-type":"item","numeric-id":1853641,"id":"Q1853641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"930dec50d296505ea5ac636cc693ba751d5d8b40","datavalue":{"value":{"amount":"+0.8306035995483398","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":"Q3543660$0BD11BB0-9AE6-4F97-ACB1-78E1D88337D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e13f94efa5a180ee860e2173b41929c73d33793f","datavalue":{"value":{"entity-type":"item","numeric-id":4231030,"id":"Q4231030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6e40133e08fd1d4167dec4cb78902bf1d400fb95","datavalue":{"value":{"amount":"+0.7961217761039734","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":"Q3543660$C9A68384-3DAA-44C8-8CC1-ADA9445F859D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"40f8ebef67abf9cc2fd8809fac112907e53de9bb","datavalue":{"value":{"entity-type":"item","numeric-id":714620,"id":"Q714620"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7e389cd1fca3d0de0f16a3047a1de72dc86a7094","datavalue":{"value":{"amount":"+0.7804372310638428","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":"Q3543660$4CF01136-4E15-4BCA-B54E-67E58F98F21B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9dfcf58ea8c1327bf5387c4d15c367eda97cc98f","datavalue":{"value":{"entity-type":"item","numeric-id":469367,"id":"Q469367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"afc9f2ff4f509ef3806a564c6eccfbdd27cedfc7","datavalue":{"value":{"amount":"+0.7605475783348083","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":"Q3543660$18ACA2F3-8861-4E22-B1BF-2018005432C9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3543660","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3543660"}}}}}