{"entities":{"Q2364690":{"pageid":2375433,"ns":120,"title":"Item:Q2364690","lastrevid":57879798,"modified":"2026-04-02T22:25:23Z","type":"item","id":"Q2364690","labels":{"en":{"language":"en","value":"Formalization of transform methods using HOL Light"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6751328"}},"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":"Q2364690$B6167F51-251A-45A4-B375-19E2744F9DBE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"000c8850eec29105937186919a6d8c379ad39a3a","datavalue":{"value":{"text":"Formalization of transform methods using HOL Light","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2364690$063E8E72-3EA9-4174-8F2C-0DBA80BA1078","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9820a921340b1e7df4baa65a308d7f8bb7eca3c6","datavalue":{"value":"1367.68255","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2364690$04F9C509-02C8-4638-A82A-25050B0BE458","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5728f1cfd1ef71e134c3ece0fb20d890bc26665f","datavalue":{"value":"10.1007/978-3-319-62075-6_22","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2364690$A3C16CCB-C6CD-4660-BC66-A872AF331D4E","rank":"normal"}],"P16":[{"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":"Q2364690$896C04F3-66C1-43CB-9C13-F765F2361222","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":"Q2364690$054DBA77-3AFA-4A60-B221-3FA141094670","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"36ae9f0663dd67e81623b5f2360b90198adfccf0","datavalue":{"value":{"time":"+2017-07-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2364690$8F607BB8-60B5-46EE-BDC1-5B46535E8134","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"37c455d82f120c8e804c5f93ff9c89922a67516e","datavalue":{"value":"https://arxiv.org/abs/1705.10050","type":"string"},"datatype":"url"},"type":"statement","id":"Q2364690$9C61DBC1-76BE-47B3-ABB1-B15AE2E947A8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2364690$F1EB8F73-DDF8-43ED-B3F2-9EB8A8804A56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed4ca2107fe9e39a03ebfd6b2537bef4a41b62ef","datavalue":{"value":"42-04","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2364690$30240DAF-9A8A-4956-837A-5FFF0706791D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"35a6a2b3f9d6c9fc8a7ac4824c020d01458d974c","datavalue":{"value":"44-04","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2364690$3B0B6E6E-8280-49D5-A8E5-377FFBB6AF23","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c874c882ca2a42d2fb4c3a898a3e6f54f491a9c4","datavalue":{"value":"6751328","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2364690$630C9233-8DED-4D90-9883-F84DF7E0EBA7","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a6f2f63e500080a6ddf193303e231e60b55ad6d8","datavalue":{"value":"Laplace transform","type":"string"},"datatype":"string"},"type":"statement","id":"Q2364690$51BD05A6-A789-4BA2-B702-6732765FA1FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"994d7c10a73037bc0ad3d751aaec1f75d12928c0","datavalue":{"value":"Fourier transform","type":"string"},"datatype":"string"},"type":"statement","id":"Q2364690$D0E24647-8937-4467-ABA4-FD9980CC5A64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2364690$2043C527-7DF3-4FE8-A576-69F17E2A8EFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"104686f3a3b63f31fa6c79f5f0116fe39fff0a7f","datavalue":{"value":"HOL Light","type":"string"},"datatype":"string"},"type":"statement","id":"Q2364690$02D75E31-2DB5-4081-8A55-EFD09FA69F70","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c652637493e8de65377ba80065ca4183c6dc627","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364690$E6EF100D-57FD-482F-8D68-97AD229FC00D","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":"Q2364690$B8D390DE-C175-4874-93A2-19ED2034C149","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8bf42d0fd66acf369e3d5d44d7ebef6adc7ae452","datavalue":{"value":{"entity-type":"item","numeric-id":56651,"id":"Q56651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364690$59BC5DEB-0479-4845-8A18-386CBC795C5A","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":"Q2364690$81EFA9CC-4C62-45B0-8660-443181F6E061","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"aec7e8ddfa11540e46efb789be0bbe2e38c499c1","datavalue":{"value":"W2618528743","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2364690$699C0339-12BC-420C-BBA9-297A748F0A21","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c383a0c029fad9b4d9ee5c58f76dd4e0097df493","datavalue":{"value":{"entity-type":"item","numeric-id":5492965,"id":"Q5492965"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364690$18BE372B-128F-4874-BF0A-96494B6FB7D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"52d3ca3104c86b480af2c0a8258502720f5e12c7","datavalue":{"value":{"entity-type":"item","numeric-id":4429927,"id":"Q4429927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364690$E9A9B371-0AF0-44FB-9320-88E8A5FBE859","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a94d54db67aeff7f5f9822e5cc5305e3d6e86d42","datavalue":{"value":{"entity-type":"item","numeric-id":3257499,"id":"Q3257499"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364690$61C19979-3910-4375-822E-DE2E73422501","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8074fcc92fbd9c3375e74173985825bb4ed621f5","datavalue":{"value":{"entity-type":"item","numeric-id":5573571,"id":"Q5573571"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364690$CCF9E0EB-51CD-4220-8FF2-5A7B8AEABC3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e1d187f2bb1c1d687b3326b9ff78435db8d4c4c","datavalue":{"value":{"entity-type":"item","numeric-id":3967932,"id":"Q3967932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364690$86D034ED-71EE-407E-841C-C7FF890BBDE8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb0f89e4608ade09fb4a027c2f09823ef5556386","datavalue":{"value":{"entity-type":"item","numeric-id":4790658,"id":"Q4790658"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364690$BFC4EFD6-0718-411E-99CC-01F70A67D460","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4804c33420ac78cc4df07fda5e1c231c8c45dfc6","datavalue":{"value":{"entity-type":"item","numeric-id":5459965,"id":"Q5459965"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364690$F8A908A7-F90B-471A-8843-3E28EAAD2095","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c81552b73ca3da654f82a5d549a003193cba99f4","datavalue":{"value":{"entity-type":"item","numeric-id":4211176,"id":"Q4211176"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364690$5F57AD0A-F7F7-4A94-9E78-D7484065CA49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9dc3d0a229a7f12036dfbbb6a0ed8a575a13c72f","datavalue":{"value":{"entity-type":"item","numeric-id":3867625,"id":"Q3867625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364690$1613E4BB-6C39-4087-B711-8AF4D96CDE36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4753702d4a1053e1a39a240a777fd8f7dd4b4b0b","datavalue":{"value":{"entity-type":"item","numeric-id":5959860,"id":"Q5959860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364690$BD467B66-B1DB-416F-84DE-F38F12D643EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4691aaf72df90fce005b56b79b724c66c0c78d38","datavalue":{"value":{"entity-type":"item","numeric-id":5449101,"id":"Q5449101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364690$A309D04D-5933-4539-9655-2394C38F15E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c10c9f71bc115df360922eb5bc721615efce0dc2","datavalue":{"value":{"entity-type":"item","numeric-id":802116,"id":"Q802116"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364690$70A056CF-A10D-48F5-979E-3FD7A7F5B372","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"995a9756826a320176f6f611c76e0ec3fbb113de","datavalue":{"value":{"entity-type":"item","numeric-id":3496717,"id":"Q3496717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364690$0077CE24-7EA3-4F25-AA4E-759E691DEF35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"51381bef73fd52769e90b7bc71f37acf33a23860","datavalue":{"value":{"entity-type":"item","numeric-id":3190549,"id":"Q3190549"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364690$DB5ED161-F77E-419F-B334-64D7B758B68B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7337a28efba559e8f6c69393bd16c1c354fee447","datavalue":{"value":{"entity-type":"item","numeric-id":2963586,"id":"Q2963586"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364690$3D1E189A-D6A0-43BB-8A5E-EF5A161AD607","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"766a111ebeb0b42bb2501047ed36561bc1dbc49b","datavalue":{"value":{"entity-type":"item","numeric-id":3856560,"id":"Q3856560"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364690$8C7863B0-163F-4F88-ADF1-5FEC7878F93A","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":"Q2364690$516CA052-4D4D-4EC0-9760-50C74EBE2907","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3d49eb451a0aa7cf50ddefb651ea8beb466724dd","datavalue":{"value":{"entity-type":"item","numeric-id":2879271,"id":"Q2879271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364690$8402FAFD-0255-4A17-8EE0-4A79CF029E4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"abadec2431bcb9018790b12c6085bfcbacdaffff","datavalue":{"value":{"entity-type":"item","numeric-id":2870169,"id":"Q2870169"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364690$82605A07-635D-4E20-895B-DED79E0F7063","rank":"normal"}],"P1643":[{"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":"8271003aae75b51aaa5835dc6429c7dbdb2d21a4","datavalue":{"value":{"amount":"+0.8164432644844055","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":"Q2364690$7986771D-68FD-448F-9EEB-3B593DBD7B83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c2749cb4c58b08c7fa045dd9e814a924984f324c","datavalue":{"value":{"entity-type":"item","numeric-id":2870169,"id":"Q2870169"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"218cdd293898734fada6a8e8f6ed3411f9788955","datavalue":{"value":{"amount":"+0.8079507946968079","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":"Q2364690$BF9017FC-65F7-404E-B2D1-B682877B6F0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"51b4c1a6cc73475e4d910067ec5b89bfb7daced5","datavalue":{"value":{"entity-type":"item","numeric-id":2829282,"id":"Q2829282"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c986984f8b87a4f6e5d7d0776c380904c1d7fa9d","datavalue":{"value":{"amount":"+0.798936128616333","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":"Q2364690$AE9F0539-31C9-4320-B3BC-7EA62FC52665","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":"26e04ea697f2d69912033c3c54f2dd3e09aaec7d","datavalue":{"value":{"amount":"+0.7978331446647644","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":"Q2364690$7908F731-9058-4273-BEBF-E5755C37D700","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6d7b6db4bf1924f8f4a4c27ad57224e0a8f56529","datavalue":{"value":{"entity-type":"item","numeric-id":2423767,"id":"Q2423767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"78a05f7d4aa59c11232b06fca67d37f03e490b2f","datavalue":{"value":{"amount":"+0.751261830329895","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":"Q2364690$E6D906F9-C7AF-4C52-91BC-020425EBF43E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2364690","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2364690"}}}}}