{"entities":{"Q3453133":{"pageid":5232533,"ns":120,"title":"Item:Q3453133","lastrevid":52400132,"modified":"2026-01-22T13:44:44Z","type":"item","id":"Q3453133","labels":{"en":{"language":"en","value":"Enabling symbolic and numerical computations in HOL Light"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6512433"}},"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":"Q3453133$4F6FA6FF-DE51-4FFE-B393-A36BFC0A3676","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7bd00acc25c5221d6d3f73028f192b1cb7ba0c8a","datavalue":{"value":{"text":"Enabling Symbolic and Numerical Computations in HOL Light","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3453133$064F3959-57E2-4DE9-AAA4-29C6A3145765","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d7e622d3b946d3974c8aaf0b53318fcd1f5d2da9","datavalue":{"value":"1417.68193","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3453133$E8BFE41D-34E8-4F2E-A044-92C6CFD23830","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"715a3ceb5f731a8bcaa62dac792f34123a60e668","datavalue":{"value":"10.1007/978-3-319-20615-8_27","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3453133$7E365057-6132-4412-8574-35C8FB1E2E2D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d6e86c607bdea4f3ca34e5ed745fe0011fa1ce52","datavalue":{"value":{"entity-type":"item","numeric-id":475383,"id":"Q475383"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453133$D139599A-1511-4E2A-97A1-31D53F542CE8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"186974f2a7f490b5339ad6dde956abae40410e6a","datavalue":{"value":{"entity-type":"item","numeric-id":3453124,"id":"Q3453124"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453133$B463C09D-4FB5-4B60-BDB3-F197450BC2BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"381b2c7fec112b57f4726817be8c4da578825618","datavalue":{"value":{"entity-type":"item","numeric-id":475380,"id":"Q475380"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453133$55A67669-334C-4DDA-BC73-7CE2BA44F082","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f0d2c11253a443ddc53e205509995096ef6b865e","datavalue":{"value":{"entity-type":"item","numeric-id":246141,"id":"Q246141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453133$5381E1A8-114E-48E5-8A60-4C997A35D1CB","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":"Q3453133$53652E48-DC55-4EB7-B09C-31396F50B0B6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7bc62645abb22752583f6909ba0e58feb505ce9c","datavalue":{"value":{"time":"+2015-11-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3453133$7FE7AC71-AEED-45C3-B487-560D5A5FC6D0","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3453133$6275F4C0-6AC6-4D82-99A0-78AC96C9026F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a50ad10d859c37581a66df0bd2c759d3d47ad6a4","datavalue":{"value":"68U35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3453133$608DAA6F-2C4B-40EE-AEB0-042D603EEA8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6be78f1bad1f2f19058dbde65eb124c0430a7d27","datavalue":{"value":"68W30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3453133$DB6A0C92-3112-4A52-8412-31BA5A643E9D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"efba16b2be07f87fd459d9799e932ccac8960a1f","datavalue":{"value":"6512433","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3453133$83DC2458-2EB5-4444-BCE8-0019989AE9AE","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"261ae6dfeffd96c9ea238e124055221c78337064","datavalue":{"value":{"entity-type":"item","numeric-id":13705,"id":"Q13705"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453133$E6C28B83-F38B-42FC-BA98-E359538362DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"29391b19386946f3f8609d95651483db905027b9","datavalue":{"value":{"entity-type":"item","numeric-id":22439,"id":"Q22439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453133$7913386E-0633-4B1D-A941-F29748CCB204","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d89eed7087f93c1cdf4120c868b02779d34eaa8b","datavalue":{"value":{"entity-type":"item","numeric-id":13309,"id":"Q13309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453133$FE08C7BA-AF6B-4702-845D-5757AC2EFBC9","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":"Q3453133$86951CF1-596D-4358-9290-A8A4EC3FA272","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":"Q3453133$0FC57F6A-C026-40D5-B652-E1C16C95019B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"045d122f7c866a2538c94085ed17e7b21daf23eb","datavalue":{"value":"https://doi.org/10.1007/978-3-319-20615-8_27","type":"string"},"datatype":"url"},"type":"statement","id":"Q3453133$7550A32C-591F-40E8-8E01-A5925F91D555","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ac48ba7f2668b3391d647c5dcab4f97dc7afa463","datavalue":{"value":"W1147542396","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3453133$7FDC8FC1-49CC-4CE7-8524-32D2B84F0830","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7714e08a8556aa1cd6a9f5fda8c7d4f8d9c37ba9","datavalue":{"value":{"entity-type":"item","numeric-id":4790649,"id":"Q4790649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453133$8C2A1876-7E3B-497A-A042-C9A4FEF0B204","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c43a14224fa5235de73a12a4a92053be887ea6ac","datavalue":{"value":{"entity-type":"item","numeric-id":1272608,"id":"Q1272608"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453133$0EDFE63F-48F7-4D86-B84A-7EA75603B581","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"19121fe5036f2676946186c6f9a088bb5b461d0f","datavalue":{"value":{"entity-type":"item","numeric-id":4227289,"id":"Q4227289"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453133$844D8323-56D3-4888-B14C-424604BE4695","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5becb9544d63b9fee8587b54b69cdd06b7a6dd3c","datavalue":{"value":{"entity-type":"item","numeric-id":4499152,"id":"Q4499152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453133$2453293A-0B51-4592-8C84-DFB638CF0D3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e5d997d3c3c1c4cbe0d251137694980cd98cf08","datavalue":{"value":{"entity-type":"item","numeric-id":1272607,"id":"Q1272607"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453133$8F99BDBB-1664-42D3-A21D-43F322C6F8A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cc5bac2a1c3bf09f6471a60799fa53f4bbb721a1","datavalue":{"value":{"entity-type":"item","numeric-id":5428262,"id":"Q5428262"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453133$EA1B7BA2-A617-4F02-B158-5C7D32B3908E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e34b8c44e244e41df1e6a71d401fe96dcb5008fa","datavalue":{"value":{"entity-type":"item","numeric-id":475384,"id":"Q475384"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453133$CA652695-81BA-458A-B853-57E5B2A1F4CA","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2fb3e22cfdea9687c7e9c67f2933def3703735b6","datavalue":{"value":{"entity-type":"item","numeric-id":5428262,"id":"Q5428262"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6669cc708ae02072641ea75cdc9c72c246b25eaf","datavalue":{"value":{"amount":"+0.7924871444702148","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":"Q3453133$6304930C-0B1F-4C2B-8EAB-D8592665EAC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"941b1236acbc8e079c1aa9b5b6f37342905adb91","datavalue":{"value":{"entity-type":"item","numeric-id":4282537,"id":"Q4282537"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b6ef8e1cd595ee73f1e385b4695826c27cc69e06","datavalue":{"value":{"amount":"+0.7632173299789429","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":"Q3453133$0E2E8AF7-B340-4128-96DF-0D8AB82595B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d6958c32e58988a08693ac87970e050d9d1ca1fc","datavalue":{"value":{"entity-type":"item","numeric-id":1272607,"id":"Q1272607"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f13fbaadac5ba83ccad0998f9425507034c869d5","datavalue":{"value":{"amount":"+0.7545784115791321","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":"Q3453133$5F8209C8-F04B-437F-A870-B86FB5FF30A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f5240345605b6df958dc529fb8dc1a54b30d31b3","datavalue":{"value":{"entity-type":"item","numeric-id":3183517,"id":"Q3183517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"81ba2936c3018c18269289a37ec29f03b5e705a8","datavalue":{"value":{"amount":"+0.7507984638214111","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":"Q3453133$E4235E48-CE88-4641-BECE-1B4B6DF0C71C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"404825eb196e28e9cdb897322b5b207a1e9328bb","datavalue":{"value":{"entity-type":"item","numeric-id":4790649,"id":"Q4790649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dae34ead2fba9d4cfa8c1866bca26d0035dc821f","datavalue":{"value":{"amount":"+0.7406637668609619","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":"Q3453133$D6C50E1A-2ABE-4F84-9E94-E12A4858BC47","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3453133","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3453133"}}}}}