{"entities":{"Q1945903":{"pageid":1956645,"ns":120,"title":"Item:Q1945903","lastrevid":69831783,"modified":"2026-04-13T10:38:40Z","type":"item","id":"Q1945903","labels":{"en":{"language":"en","value":"The HOL Light theory of Euclidean space"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6154928"}},"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":"Q1945903$60E8918C-CCDB-4EA6-8634-589C2F990B26","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e766cafdaf95a6ae38cbfe7fff0ba5a21549eb89","datavalue":{"value":{"text":"The HOL Light theory of Euclidean space","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1945903$17A1FE12-5409-41C7-9F72-C3939CA36F54","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6a8f6bea00b9785ef7b68d34f5ed930903a099c0","datavalue":{"value":"1260.68373","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945903$A73E9376-1496-431E-9C1F-D287DFA2883D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cc45e6b9322bed7360e4aac2a42f8c73614b44f3","datavalue":{"value":{"entity-type":"item","numeric-id":1787138,"id":"Q1787138"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945903$321C9B5A-8D25-4161-A6BB-F503D850BB1C","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":"Q1945903$1E5CBB5C-C3CB-409C-81B2-A8043705A03D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4bad757aec17a8570e2102d57df4c93baefd6019","datavalue":{"value":{"time":"+2013-04-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1945903$59A95690-6FA6-48B8-91FA-2793F62A8F71","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945903$E23B0B36-A87C-4897-BBAE-0DD6D9E1FB83","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1e5157b27f85e259ea8b2a6f555fd5ec7c3a7ebc","datavalue":{"value":"6154928","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945903$1A9D60AD-5845-4739-816F-81AC752232F8","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c3a96a510fd7a7846523150dd8bb125ef8f415fa","datavalue":{"value":"formalized mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945903$7833DEC0-B096-42FF-9EDE-16A41DEE2B33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a9b86cd84094b9b213d4cc4362fa44d5551f4bf2","datavalue":{"value":"Euclidean space","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945903$1591BE67-ED31-43E1-A657-7BA26C1CA964","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5caf09f23a5bd44601ef1b376fd6cba9845252d5","datavalue":{"value":"vector space","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945903$4294F567-8A81-4192-92BA-2480DB1A7EF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7c8099541f1cabb374567a4c1f9fb4dfc5885e5d","datavalue":{"value":"\\texttt{HOL Light}","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945903$A210612F-3984-40EF-B0C1-4296A10F7A75","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19c3232540dc15c9350e8393498317de25361cb2","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945903$BD850A6C-71CF-4A6E-A6C7-086687D2DF25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9b0860d94af5fdff4b5635709ae334aacdf07ca1","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945903$D26A360F-8B47-4894-93F7-2E285F303A38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"66eb045e037081b6f6e8499f9fef44d8fbb7e0b0","datavalue":{"value":{"entity-type":"item","numeric-id":22240,"id":"Q22240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945903$12DDE925-647F-4FB0-92F6-708EE8384126","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":"Q1945903$F61069E5-57EE-4163-96B9-97483F64B0C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9301974fbdbf3896f705a4c8ed840f169a9b63f","datavalue":{"value":{"entity-type":"item","numeric-id":19182,"id":"Q19182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945903$EE891748-B430-438B-89CF-5696CFB422C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"af3b5ddb4818ec81bb9bea3bab4852742bff1bd5","datavalue":{"value":{"entity-type":"item","numeric-id":22101,"id":"Q22101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945903$A16EF55C-E187-4712-AB21-26ACEF6D6BF7","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":"Q1945903$C2829942-AC5F-49AA-A907-5B1098E8915A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"07f544da61a733e790b6290335bb2f4a402f91cc","datavalue":{"value":{"entity-type":"item","numeric-id":35395,"id":"Q35395"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945903$6D7AC7BE-562C-465E-AEAF-F0F58E6B2D08","rank":"normal"},{"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":"Q1945903$2E0D9371-38E9-433B-B70B-0FD947A12A06","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":"Q1945903$69F1FC6F-2073-4DAC-AF3A-1C478B6AD3BF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7e56017848ef8cefd15dcb624a5f716ea4714540","datavalue":{"value":"https://doi.org/10.1007/s10817-012-9250-9","type":"string"},"datatype":"url"},"type":"statement","id":"Q1945903$0F991DDF-3EDC-428A-BAD6-1ECE8F0E2E8C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"63a43ea94dc9ed0b89c54d653e4d3230ce2e78a1","datavalue":{"value":"W2091456056","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945903$0E567E1F-BC55-4F5E-9829-2AACBFC96158","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"62b4619cd90eab2ee99da46e38d86e9871623db6","datavalue":{"value":{"entity-type":"item","numeric-id":4736392,"id":"Q4736392"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945903$082DA417-AF21-4021-ADA7-A8A89816A0B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"67a0619f07c8313163d5395382f74c59a1da4d00","datavalue":{"value":{"entity-type":"item","numeric-id":5448058,"id":"Q5448058"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945903$0A5004CA-3194-4728-B6CF-49BF98A63F4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"63983f76bcac6e0c986bd71036b36fda64f6bd04","datavalue":{"value":{"entity-type":"item","numeric-id":977177,"id":"Q977177"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945903$84376ABE-60B4-49CA-B213-711949F7047D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a5e182d22cd63374751049cb1ad374f0b5175f7","datavalue":{"value":{"entity-type":"item","numeric-id":5477650,"id":"Q5477650"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945903$01F37677-E97D-4A0B-B06B-B3500C68D43D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a8e615433d7c0da849d212b92d36df1a27bb8523","datavalue":{"value":{"entity-type":"item","numeric-id":3183516,"id":"Q3183516"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945903$0A0D5CBF-31E2-4526-9E80-AD8071C20A09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14084b41dac7e71956551690bb40c48e6f7029ba","datavalue":{"value":{"entity-type":"item","numeric-id":5747657,"id":"Q5747657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945903$42360AD0-B082-482C-A571-873666059B66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f8afeca6176bd71f678fdde07e3ce13aeb97dc8","datavalue":{"value":{"entity-type":"item","numeric-id":3845873,"id":"Q3845873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945903$6EFE6A9F-9E63-4563-A795-11CBCC095DA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce0bea36a0ced271d66d350d87a64d0048c37bd9","datavalue":{"value":{"entity-type":"item","numeric-id":4218971,"id":"Q4218971"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945903$5E5B2E64-B447-4A66-8AF0-4A363E2CA2C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e9c607582a152b176d61f4654f7cd514db2bc8ff","datavalue":{"value":{"entity-type":"item","numeric-id":4258069,"id":"Q4258069"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945903$D499341C-9005-4696-85DB-2A0CF563737A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"08224f858fdc314170f06ece60c04983ab8a019b","datavalue":{"value":"10.1007/S10817-012-9250-9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945903$C39A34E6-AF40-421F-97AE-2F8382926822","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"030a8e9ac6fc09570217d40508a4a4eabc57af6f","datavalue":{"value":{"entity-type":"item","numeric-id":5477650,"id":"Q5477650"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fbf88e9c9ed833a60cbee62023d9706221270c58","datavalue":{"value":{"amount":"+0.9012302756309508","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":"Q1945903$5C051B87-6FC1-4B4F-9BDF-36B30975511E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"647c8d4704e4e1c63c4d44857f4efc2289373760","datavalue":{"value":{"entity-type":"item","numeric-id":682381,"id":"Q682381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"89e3cbac0f6c8fdf9a13731428feeaf8a023b48e","datavalue":{"value":{"amount":"+0.790221095085144","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":"Q1945903$B339D032-2457-4B3F-BAE0-3E673BCAE4BD","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":"6e3826878fe9fe6424c444f67ac8a7a9eca64e8c","datavalue":{"value":{"amount":"+0.7383424043655396","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":"Q1945903$8C7372D7-A490-4BE3-9F51-3AB7BA5F79C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6f9dafd7c7f113b48c000ccbff4d8ebda68a39d4","datavalue":{"value":{"entity-type":"item","numeric-id":438546,"id":"Q438546"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f9f93736113a348962ef98d7519d8dffb51ba1c6","datavalue":{"value":{"amount":"+0.7272322773933411","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":"Q1945903$0096725F-C74E-40CD-A98A-20928687EC6D","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":"cbcd1a8c07f57080052cce8f1b3cea4a9dd1d635","datavalue":{"value":{"amount":"+0.7260714173316956","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":"Q1945903$0C19C270-E3B7-4B75-A2D6-C45BD8A04BDA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The HOL Light theory of Euclidean space","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_HOL_Light_theory_of_Euclidean_space"}}}}}