{"entities":{"Q2375439":{"pageid":2386182,"ns":120,"title":"Item:Q2375439","lastrevid":73762140,"modified":"2026-04-14T17:10:55Z","type":"item","id":"Q2375439","labels":{"en":{"language":"en","value":"Formalization of linear space theory in the higher-order logic proving system"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6175758"}},"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":"Q2375439$18B3DC0B-CA66-4B55-8BF0-AD809F623E44","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b98c651c4c4000a9b477e21f97b8477df53134f2","datavalue":{"value":{"text":"Formalization of linear space theory in the higher-order logic proving system","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2375439$8943EFA9-6A24-4A3B-BAEE-6066C0431D6E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4c41f5d9fb1a824d7765c27dfe1b510c4c928462","datavalue":{"value":"1315.03021","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2375439$EC900506-24F8-4666-A627-EA55F8DE88B2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"79b3279e54c91e3d89f129d9d4f20e4a3ffec9e3","datavalue":{"value":"10.1155/2013/218492","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2375439$EB43DF8B-1D13-459F-999F-7C5335D5F79C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d39b4536ab4b3691fa10e20a21c234518780f867","datavalue":{"value":{"entity-type":"item","numeric-id":1665985,"id":"Q1665985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375439$1CD443DE-8667-49A0-8ED7-6BED4C43DBFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"835b10677da990f913c3325a9e98126315b94807","datavalue":{"value":{"entity-type":"item","numeric-id":2375438,"id":"Q2375438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375439$7ED27E3D-298B-4C33-88C8-ECB0D83FCD59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bad697f6be27ac07cc0bac5f2074dc40ed884baf","datavalue":{"value":{"entity-type":"item","numeric-id":258539,"id":"Q258539"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375439$9AFA49A0-958D-417F-AC70-8DD1619436FB","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"bb299feb2b87699ac8beef494c52fd2765eaf609","datavalue":{"value":{"entity-type":"item","numeric-id":118601,"id":"Q118601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375439$9638F3CF-BAC6-49EA-A237-F434FC0FD79F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b84d2a34981f1c1a0d0fb543ea5aabc14a21194b","datavalue":{"value":{"time":"+2013-06-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2375439$AF6A7535-F6F9-4455-A989-E4A9E89DD3B8","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"5f70c8d1ff02b7df4e33884a6065af05c735e4df","datavalue":{"value":"The authors present a standard application of HOL4 to a new domain, linear spaces (i.e., vector spaces). They proved 37 standard properties of vector spaces such as the uniqueness of zero (which is also used as the leading example for the presentation of the work), that multiplying an arbitrary vector by a zero scalar results in the zero vector, or that any scalar multiplied by the zero vector results in the zero vector.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2375439$C95C79D1-D4AA-42AD-AE53-37023B7786AE","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"80e987276e122a41f9b91b8b2fac713fac5a8dbb","datavalue":{"value":{"entity-type":"item","numeric-id":504392,"id":"Q504392"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375439$2C60CB82-FD45-4414-91A8-3C0BD704754B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2375439$CAB7AC77-8AFC-4344-A949-068A69E7820F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2375439$7AA50CC6-5C49-45B6-8FE1-4BE9B9828F72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2375439$E2F845B9-510E-4379-9AA5-C0923F2257B6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3076af0b88f3b1b5921346200427e0cf228ab138","datavalue":{"value":"6175758","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2375439$444A2631-A378-4993-A665-FC79E7E14421","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"01873808ed420453ae082d7e18447e172733687b","datavalue":{"value":"higher order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2375439$F78022A2-3100-49E0-8809-A91970165E76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2375439$565A7132-9004-495C-A9BC-1FA9E8A9CB4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4ee42c95fb4dd331a6fe625189ea56ec215d8623","datavalue":{"value":"vector spaces","type":"string"},"datatype":"string"},"type":"statement","id":"Q2375439$7B542C98-8A56-4DFD-91F5-BEDE0093442C","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":"Q2375439$F8C4AEBF-4AE7-445E-93F5-2B20F5DD2A92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375439$F81F4121-A047-48D3-B8C4-510C423F336F","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":"Q2375439$9A0374BB-585A-47FA-811C-98688B43886C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fb1193fe6975e801b57adbe99f8ded61a3b71301","datavalue":{"value":"https://doi.org/10.1155/2013/218492","type":"string"},"datatype":"url"},"type":"statement","id":"Q2375439$97258E79-9BA8-4569-AE7F-859E4B748C56","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"05fb784a87eb7bef2f1fc0eb1f58e691e2fc2d52","datavalue":{"value":"W1981373951","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2375439$67DDBAD5-583C-4436-B5D8-3D6DF2CD4ACE","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"31bfc122c1605d99996368ad6e8854dca22e4008","datavalue":{"value":"Q59002164","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2375439$DF528725-1690-4FDA-A426-38D6B7624307","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6496304f13783e82d12a275120aa4626825ea47b","datavalue":{"value":{"entity-type":"item","numeric-id":4231030,"id":"Q4231030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375439$94267A9E-052A-42A0-9381-2EDD461C24CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c204802beb45179cdf9d51e6bccbe83dc656952c","datavalue":{"value":{"entity-type":"item","numeric-id":816219,"id":"Q816219"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375439$3251FCB7-9F96-4B53-9AD7-18E3F30337BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77f4334b25d43b9293350a877e2d317280ca55a9","datavalue":{"value":{"entity-type":"item","numeric-id":3543646,"id":"Q3543646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375439$6AA00477-0669-4EB6-8B57-468089A57F89","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4d5a298f24996e765d38d2efeed8299436b97d4f","datavalue":{"value":{"entity-type":"item","numeric-id":1106836,"id":"Q1106836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b61698d382ee014735fb4e9cf35a4b319eeb2d4e","datavalue":{"value":{"amount":"+0.89738774","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":"Q2375439$051904CB-5819-4DBA-8E55-3596DC65C41E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ec4b4e126c2d0ced1d7e3dcc88e4ffcc7396c754","datavalue":{"value":{"entity-type":"item","numeric-id":4244309,"id":"Q4244309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6daf3f68156f1b130dae853e0b9861af7ad7874d","datavalue":{"value":{"amount":"+0.8938415","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":"Q2375439$D07F3FB3-5A29-4111-A069-EC5FA2C30300","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9a7ebe750efa17eec7129d8dc648916fa37660af","datavalue":{"value":{"entity-type":"item","numeric-id":5179015,"id":"Q5179015"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c7ee41ed6a8010c51f341e441bbbbdc428c7dea1","datavalue":{"value":{"amount":"+0.891011","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":"Q2375439$B48BA74F-497F-4EB7-9C7D-FE7DDD3D5386","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"80b44a08bec48344b2562fc1b487c788db7bd5fd","datavalue":{"value":{"entity-type":"item","numeric-id":2424887,"id":"Q2424887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f1d95f867f118f109f882fd2b5db052eb976e85c","datavalue":{"value":{"amount":"+0.88548756","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":"Q2375439$8B0B5A18-1CC9-490A-B299-EAF1B9072830","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dd9d4223dd3227b10018b637dae5c80fa8ce1b2e","datavalue":{"value":{"entity-type":"item","numeric-id":4291039,"id":"Q4291039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d7ee92befae575fca7bfa313096fdb9aee617995","datavalue":{"value":{"amount":"+0.8849502","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":"Q2375439$7FBA0CAD-A909-4A22-812F-CD0C1692BEF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fd878339f0eb07087b6396daf9a134907762719c","datavalue":{"value":{"entity-type":"item","numeric-id":469998,"id":"Q469998"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5e653b1e15d7ab9304982bdb0952ab8f9a366262","datavalue":{"value":{"amount":"+0.8848193","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":"Q2375439$9806C3A9-7AF6-4A1E-A033-A89FEFDA02F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8f58d5e1ac65ae4230a0a40dd416bc257fae2485","datavalue":{"value":{"entity-type":"item","numeric-id":2883080,"id":"Q2883080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5b4152fe4b8bcd2c5889fc632c7259efcd4c0004","datavalue":{"value":{"amount":"+0.88412565","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":"Q2375439$D6900952-1C81-4771-8F92-17819C2FA874","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9da77fb6e753ee6b08ebfa782466c6162d9fbc28","datavalue":{"value":{"entity-type":"item","numeric-id":5688795,"id":"Q5688795"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0d41b717341d1a6c5c2b1a370478b6b108cc91b1","datavalue":{"value":{"amount":"+0.88361037","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":"Q2375439$27E74E80-3630-4499-B7EE-8D1D49B300D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b9b8f364d0ce24d4957868e5fc73a88e93d220e4","datavalue":{"value":{"entity-type":"item","numeric-id":3408152,"id":"Q3408152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"900b8c20d73feaf9fd34fdc1d0b6b0acf884ecdf","datavalue":{"value":{"amount":"+0.8834872","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":"Q2375439$FB439539-B490-450A-A427-6ED3E63DF68B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1eb2102511dec07fb34f4d057bfc8c8f969e5375","datavalue":{"value":{"entity-type":"item","numeric-id":2503319,"id":"Q2503319"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"900b8c20d73feaf9fd34fdc1d0b6b0acf884ecdf","datavalue":{"value":{"amount":"+0.8834872","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":"Q2375439$59CCFDE2-3ED0-4315-8718-0A4EB531A305","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375439$3913F43A-E261-436D-BA1C-D9D19E4D81CE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formalization of linear space theory in the higher-order logic proving system","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formalization_of_linear_space_theory_in_the_higher-order_logic_proving_system"}}}}}