{"entities":{"Q1666338":{"pageid":1677079,"ns":120,"title":"Item:Q1666338","lastrevid":70784235,"modified":"2026-04-13T17:02:43Z","type":"item","id":"Q1666338","labels":{"en":{"language":"en","value":"The formalization of discrete Fourier transform in HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6926988"}},"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":"Q1666338$530331EB-B61C-4BBF-A745-6DBF230332B2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2b33a277c848a655292685e7a22cadc58c9e19c6","datavalue":{"value":{"text":"The formalization of discrete Fourier transform in HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1666338$BED6DB25-8E39-42F1-98E0-9DAE3F29FBBF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d09bdf41ffa26bf90355fd7294e6122d9f63d7d9","datavalue":{"value":"1394.68353","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1666338$25B0EFB4-538B-40AC-9FF8-8445087B245A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"958eb457cadae5e423587ab1dbbd2c522f86b706","datavalue":{"value":"10.1155/2015/687152","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1666338$E0C9779C-3BA9-4D35-A4D2-AE9C3568DF8F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fb41e43426ff3ff3f8a93f102f45b1fd00efc7eb","datavalue":{"value":{"entity-type":"item","numeric-id":826357,"id":"Q826357"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1666338$E9575A31-B611-4EBA-847D-0D8CD8B59441","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":"Q1666338$8ABACF2F-2B01-4502-9635-2B55DBDDE531","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0e172baa8338e96dcedaaa760e0a854bf37592da","datavalue":{"value":{"entity-type":"item","numeric-id":1327821,"id":"Q1327821"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1666338$80562C65-48A7-4A10-A951-BFAD137434FD","rank":"normal"},{"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":"Q1666338$3C45046C-6E54-4890-91AB-36881CCE0030","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"50d652e4e16e06d3074fef782359eca688cb5a60","datavalue":{"value":{"entity-type":"item","numeric-id":494541,"id":"Q494541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1666338$700E448D-BBBA-4461-B309-A301C2586F8C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3dc97bc0aff607b9c22ce37ffa18b6de85001d90","datavalue":{"value":{"entity-type":"item","numeric-id":86199,"id":"Q86199"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1666338$439A24D6-1D43-4A58-8051-9C044AE44447","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"07d78b2809f727a96c8c6621733f1ab3a1973328","datavalue":{"value":{"time":"+2018-08-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1666338$7603B504-1CCE-483B-B3EA-50018D853661","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"b81e388e281881d154e3e2010ea814524f240fa4","datavalue":{"value":"Summary: Traditionally, Discrete Fourier Transform (DFT) is performed with numerical or symbolic computation, which cannot guarantee 100\\% accurate analysis which may be necessary for safety-critical applications. Machine theorem proving is one of the formal methods that perform accurate analysis with completeness to some extent. This paper proposes the formalization of DFT in a higher-order logic theorem prover named HOL. We propose the formal definition of DFT and verify the fundamental properties of DFT. Two case studies are presented to illustrate usefulness and correctness of the formalized DFT, including formal verifications of Fast Fourier Transform (FFT) and cosine frequency shift.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1666338$A5D3B811-E97E-4EB4-9C33-BE36CBE2EF2A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1666338$76B66224-5830-4E6B-8ADA-8208F4C85D3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c4603c40f3b09770fdbb70ee2650f252415f25c5","datavalue":{"value":"65T50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1666338$DA67DDE7-DC56-4C92-8108-E087CFE338DD","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d0e4ec6412cfe43a3bfb1b8f981a256d5ee686b5","datavalue":{"value":"6926988","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1666338$E3D1CA99-D89D-4B96-88E2-26797001A40D","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"6cefc87c6bff69c64c7e924e63958a94a1c688f6","datavalue":{"value":"Q59118930","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1666338$A74640B5-6A45-4ABB-8C1A-1E2403406303","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":"Q1666338$530EE9AD-60D1-41FB-9665-69D33DF8AEDE","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":"Q1666338$C37F4BE6-B2D4-44F9-A0F6-205A093A8D39","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":"Q1666338$B5CB7416-35CB-44D6-A137-D62D9DB42ED3","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":"Q1666338$6CE7E353-0D28-4DA0-BC45-2F0A162FE9E3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7aee8aa95ba87cedffdb65933ad15a4f5a9d7af1","datavalue":{"value":"https://doi.org/10.1155/2015/687152","type":"string"},"datatype":"url"},"type":"statement","id":"Q1666338$84FD0718-D3B8-408A-A924-E8CB7A0D7162","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d5b063924c8191a92c42f1fa323a688f6e455945","datavalue":{"value":"W1880321261","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1666338$5560BE81-EC47-4897-87EA-4EFFC77BAADA","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":"Q1666338$451A15E7-B979-4561-B3E5-33F18F71D801","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c4ce95b5c801e45ae9bbe76240e216f627513de","datavalue":{"value":{"entity-type":"item","numeric-id":2434565,"id":"Q2434565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1666338$6DC0658F-480D-457B-AA6A-B9FB182ADA78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7f9b906283b7665f271b7a544725c3b2848a7d1","datavalue":{"value":{"entity-type":"item","numeric-id":4818806,"id":"Q4818806"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1666338$90807369-C5E2-4201-8FC9-86CF076A1C40","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":"Q1666338$F39A85F3-E384-46E3-B1CA-1AC294B66EAB","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":"Q1666338$BFED3780-6456-4C21-8FD8-36A891FC2A67","rank":"normal"},{"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":"Q1666338$CD09A5BF-95EB-4D34-B858-0C66121C9AB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"027661121afc8ca039752afc0a4269a02976c160","datavalue":{"value":{"entity-type":"item","numeric-id":1334896,"id":"Q1334896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1666338$82203202-D711-422B-B757-1683A7FD4275","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3b819f2c80f9e04e31e7f8a5919a6260d006131e","datavalue":{"value":{"entity-type":"item","numeric-id":2294128,"id":"Q2294128"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1666338$46739A2E-9466-42C1-B8F4-7FB21DAA3FA7","rank":"normal"}],"P1643":[{"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":"b883559e9f95f7ee407238f0cf95a1a330ba11c1","datavalue":{"value":{"amount":"+0.807248592376709","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":"Q1666338$6498FC5B-2ACA-451F-8364-9C9C070114E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"764c246a1e922833020056c629835fdd29caec98","datavalue":{"value":{"entity-type":"item","numeric-id":5492965,"id":"Q5492965"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"06e4a8884b96aab3425e8575e5c8a71a47f0c244","datavalue":{"value":{"amount":"+0.7933529019355774","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":"Q1666338$13F997A7-2004-4434-8924-7F5225042C13","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":"31058e6cb8408b23510668c7d33fe0dc2a1cecc3","datavalue":{"value":{"amount":"+0.7626693844795227","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":"Q1666338$A4AD124F-0CD3-40E6-A1CB-077BE06F92BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"97ffca00c7848a047cec838a74c50514c4ed10f1","datavalue":{"value":{"entity-type":"item","numeric-id":2879271,"id":"Q2879271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"63be0e93cbea0d6e7241ccd595c5b4d9dc957d0a","datavalue":{"value":{"amount":"+0.7440922260284424","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":"Q1666338$A828EFAB-BDF6-42B8-87C1-084C9859D283","rank":"normal"},{"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":"72fbca63b3b48199d2113589853a6f962105ecc8","datavalue":{"value":{"amount":"+0.7167477011680603","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":"Q1666338$86E8251C-40B0-47DA-B320-5ED8B7E3B9A5","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"daf5f856a5d861312ad309ab567540337a5f61d6","datavalue":{"value":{"entity-type":"item","numeric-id":57050,"id":"Q57050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1666338$55F893A5-A000-4AFF-91F0-C194E763B1F0","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The formalization of discrete Fourier transform in HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_formalization_of_discrete_Fourier_transform_in_HOL"}}}}}