{"entities":{"Q6159364":{"pageid":13294196,"ns":120,"title":"Item:Q6159364","lastrevid":58723425,"modified":"2026-04-06T11:40:26Z","type":"item","id":"Q6159364","labels":{"en":{"language":"en","value":"On the formalization of the heat conduction problem in HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7691288"}},"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":"Q6159364$48CADDF7-7CFA-44DF-BE3A-581A80E011C7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7bb0d35333b9ad32d0fc14d3abc63ed1fc1c20eb","datavalue":{"value":{"text":"On the formalization of the heat conduction problem in HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6159364$AF3D02D5-DA0B-4F10-8B98-ED5A634E9596","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"19ecd3db0c0d3a5762d989641bfce01a969f14b6","datavalue":{"value":"10.1007/978-3-031-16681-5_2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6159364$3E7C32E7-D4CC-440B-B37D-C3E212B43D6F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1757b7858abbd82f1a7b672a3c55c6c861ee6788","datavalue":{"value":{"entity-type":"item","numeric-id":6159363,"id":"Q6159363"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159364$28DD1E03-81E6-41C0-ABD9-E4F64C1C8650","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"891b3bc2f96589c9dedada7f9b5bb76f55e7c5a3","datavalue":{"value":{"entity-type":"item","numeric-id":1640639,"id":"Q1640639"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159364$E98741B7-A3E0-4E9C-8D28-0E266FD369A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"393ef07e7673f4510d0e5689d2d44001b3ecc236","datavalue":{"value":{"entity-type":"item","numeric-id":246140,"id":"Q246140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159364$B5190A74-6E80-46E2-9E4C-27AE93259A26","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":"Q6159364$8AC61EB9-53C7-462B-8F9C-6B8A8483A350","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":"Q6159364$35454CA0-7D62-4000-B1B2-FE10A0D4A997","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4fa95a2618f91e175d2e6cdf4f6ce4782d828b01","datavalue":{"value":{"time":"+2023-06-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6159364$A1DB0B17-5BB3-4F63-84D1-609056FFCBD2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"cb88ac2b7a830721a99012e6c933ac9f6833a949","datavalue":{"value":"https://arxiv.org/abs/2208.06642","type":"string"},"datatype":"url"},"type":"statement","id":"Q6159364$5956BAAE-1904-412F-9B00-B2A4915F677E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"51b7800ccceb407b4c9aa81c10252a3a04dbfebf","datavalue":{"value":"68Vxx","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6159364$0FF8F0F0-03CD-40D0-9958-A6BE89D146BA","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"088b1511b3257a0aff96f97b68a8451d8c2b286c","datavalue":{"value":"7691288","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6159364$DBCFAE01-3D1D-4C5D-BD65-97EB879AEBA3","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0d3373f8b8896e69ba2657108b1229cfe87c9662","datavalue":{"value":"heat equation","type":"string"},"datatype":"string"},"type":"statement","id":"Q6159364$048C64E4-1218-43F8-933A-6A6240B78A99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ad346b95e27c3ee411106fd0b9ec9f4ceac33a0e","datavalue":{"value":"partial differential equations","type":"string"},"datatype":"string"},"type":"statement","id":"Q6159364$7D784C51-6CC7-4045-9083-7DF51F048B82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"223c894e2b3459e61b72e879a858aaa95a17cb51","datavalue":{"value":"separation of variables","type":"string"},"datatype":"string"},"type":"statement","id":"Q6159364$C4EB11DC-2635-4DBB-AB80-7DB23A3C5AB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q6159364$9E875FC5-F183-4684-B46A-36BCDE5A6296","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q6159364$B674D98A-D3E6-43D7-9C2B-F0CAEB171956","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"104686f3a3b63f31fa6c79f5f0116fe39fff0a7f","datavalue":{"value":"HOL Light","type":"string"},"datatype":"string"},"type":"statement","id":"Q6159364$05910C8B-61FB-4D3C-86D9-4EEEFF58F11B","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":"Q6159364$966666E3-4374-47BF-97E9-DA62CCF2E32B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"079477af4519300e4cabe52f3ba503dab0900ccb","datavalue":{"value":"W4296050254","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6159364$5AB8EDB9-F89E-4978-9ED6-19EDC8830B25","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"47dc89715e3e3cd3422b85db39d9100326217399","datavalue":{"value":{"entity-type":"item","numeric-id":5901991,"id":"Q5901991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159364$833571A8-C6D8-4A19-9D1B-1F689F27E219","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cebee4f5079038a332edd13c8b34af2c6d5ab9ad","datavalue":{"value":{"entity-type":"item","numeric-id":3696432,"id":"Q3696432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159364$C9E39F5C-4025-4C0A-A9A1-AA0A3E64B62A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c56997e260a26f43f8453507b961ac2ab6459e3e","datavalue":{"value":{"entity-type":"item","numeric-id":3566755,"id":"Q3566755"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159364$EDC51FDA-7594-46F6-B309-DE9F432A2C19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"261b2e3ec06bb75337e2ce4ddddcaf9edd69e7b2","datavalue":{"value":{"entity-type":"item","numeric-id":5189317,"id":"Q5189317"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159364$C9C21C8E-9DF9-48F2-A242-A5E9C20182E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"848dbc976b0976db4f72071eeb6590e4f9fd9099","datavalue":{"value":{"entity-type":"item","numeric-id":5313371,"id":"Q5313371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159364$5A4AC62A-110F-44AE-BAF0-510F6CF10FFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03cb8e50e6c3bd60a9a9a59407cf30e8e788baa4","datavalue":{"value":{"entity-type":"item","numeric-id":3618853,"id":"Q3618853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159364$950BFAFA-6A38-4733-9CA1-C9D2ADB2D845","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47b6f4b63bc26052368e7b5944153c26fe1fa531","datavalue":{"value":{"entity-type":"item","numeric-id":2914756,"id":"Q2914756"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159364$9C279986-8780-47EB-8283-BF5A9887B264","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6974134b0a79f0a7c99fc8d68a2c66295fb57263","datavalue":{"value":{"entity-type":"item","numeric-id":1722644,"id":"Q1722644"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159364$B04E1AAD-2056-42AD-886A-283EC6A94165","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6bc678670516baea1e66c96ed06cf7bb53acabcd","datavalue":{"value":{"entity-type":"item","numeric-id":2031406,"id":"Q2031406"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159364$2D9D7C93-02E3-4029-8AD2-CD630DF5CEC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9944419ddca97bb1a983c58293765864b8d9d27e","datavalue":{"value":{"entity-type":"item","numeric-id":2364690,"id":"Q2364690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159364$0C0843E8-69CB-418A-B6A5-3C1C6D49C37E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"21ac3f278c08c1e4a574dccacc016161bf56f67a","datavalue":{"value":{"entity-type":"item","numeric-id":2829282,"id":"Q2829282"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159364$F511157C-7A60-4DEF-ACBC-952A6A3B61EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f61ec795bf8abab1978c4909f302e2d4340af01","datavalue":{"value":{"entity-type":"item","numeric-id":5747647,"id":"Q5747647"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159364$812C0D74-041B-4587-9821-D517D2D30825","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"230b7fc18a749f4eebf9b83b210fe499e9046d79","datavalue":{"value":{"entity-type":"item","numeric-id":2398899,"id":"Q2398899"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159364$27D7110A-4382-4626-B71D-716BC13451C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a773138066a776d8468cab99cc8cd0eda548164a","datavalue":{"value":{"entity-type":"item","numeric-id":2416853,"id":"Q2416853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159364$D687DFA0-76BC-411E-8168-130826BAA49C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"83dc56f3406c9fc3c1bc27825572e647ef3c31f0","datavalue":{"value":{"entity-type":"item","numeric-id":786994,"id":"Q786994"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159364$B3FAEB8F-9E94-412F-B53A-4DF9802A581B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"70d5a248b81548c71c7ef34a7a0039cfb3f2445b","datavalue":{"value":{"entity-type":"item","numeric-id":1579923,"id":"Q1579923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6159364$AABF93E1-E7CE-4CBE-8875-71A5D97D0617","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"40a358107e0aa52d0d1913166ea142904824186e","datavalue":{"value":{"entity-type":"item","numeric-id":2364690,"id":"Q2364690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bb6d4616aaf6b50748c31338c19b13d2d57fac23","datavalue":{"value":{"amount":"+0.6632332801818848","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":"Q6159364$3127B60A-5706-42BF-99F4-E9BF5BC0C105","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad617f4867ba25c0dbef4c11fe4a2485819f46b8","datavalue":{"value":{"entity-type":"item","numeric-id":5869574,"id":"Q5869574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cabe0fc17a9da78c8ef5b0c7758015304af807cc","datavalue":{"value":{"amount":"+0.6630662083625793","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":"Q6159364$5E6F3EE7-B68A-4CBC-8794-811E2E6D5679","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"76119a1c36c396eccec926d14e823fbc0fe16af1","datavalue":{"value":{"entity-type":"item","numeric-id":2031406,"id":"Q2031406"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b577967b22de9fa3a68fdbd517025147f0728a25","datavalue":{"value":{"amount":"+0.6415579915046692","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":"Q6159364$13239111-18F8-4EB1-BF4C-5A284B8DF45E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f75593fc7091fd7b5f9d18544a3d3a394ace3d91","datavalue":{"value":{"entity-type":"item","numeric-id":1640640,"id":"Q1640640"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"568fbc2e9b92b0f4e461fd9e124ef9446c580a83","datavalue":{"value":{"amount":"+0.6412490606307983","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":"Q6159364$EFEC1E44-6DBF-4DB3-BA93-826BE6D8985D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"895f01dbe4514afaf4e58308193c557e5a7e265f","datavalue":{"value":{"entity-type":"item","numeric-id":2375439,"id":"Q2375439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"58a519d2f5494886cf13c5b031b8e0cc6b7e4923","datavalue":{"value":{"amount":"+0.6367038488388062","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":"Q6159364$76147C87-9ED5-467D-9F12-0626674AADCF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6159364","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6159364"}}}}}