![](/images/graphics-bg.png)
The Formalization of Discrete Fourier Transform in HOL
المؤلفون المشاركون
Guan, Yong
Zhang, Yupeng
Li, Liming
Zhang, Jie
Shi, Zhiping
المصدر
Mathematical Problems in Engineering
العدد
المجلد 2015، العدد 2015 (31 ديسمبر/كانون الأول 2015)، ص ص. 1-8، 8ص.
الناشر
Hindawi Publishing Corporation
تاريخ النشر
2015-10-28
دولة النشر
مصر
عدد الصفحات
8
التخصصات الرئيسية
الملخص EN
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.
نمط استشهاد جمعية علماء النفس الأمريكية (APA)
Shi, Zhiping& Zhang, Yupeng& Guan, Yong& Li, Liming& Zhang, Jie. 2015. The Formalization of Discrete Fourier Transform in HOL. Mathematical Problems in Engineering،Vol. 2015, no. 2015, pp.1-8.
https://search.emarefa.net/detail/BIM-1074468
نمط استشهاد الجمعية الأمريكية للغات الحديثة (MLA)
Shi, Zhiping…[et al.]. The Formalization of Discrete Fourier Transform in HOL. Mathematical Problems in Engineering No. 2015 (2015), pp.1-8.
https://search.emarefa.net/detail/BIM-1074468
نمط استشهاد الجمعية الطبية الأمريكية (AMA)
Shi, Zhiping& Zhang, Yupeng& Guan, Yong& Li, Liming& Zhang, Jie. The Formalization of Discrete Fourier Transform in HOL. Mathematical Problems in Engineering. 2015. Vol. 2015, no. 2015, pp.1-8.
https://search.emarefa.net/detail/BIM-1074468
نوع البيانات
مقالات
لغة النص
الإنجليزية
الملاحظات
Includes bibliographical references
رقم السجل
BIM-1074468
قاعدة معامل التأثير والاستشهادات المرجعية العربي "ارسيف Arcif"
أضخم قاعدة بيانات عربية للاستشهادات المرجعية للمجلات العلمية المحكمة الصادرة في العالم العربي
![](/images/ebook-kashef.png)
تقوم هذه الخدمة بالتحقق من التشابه أو الانتحال في الأبحاث والمقالات العلمية والأطروحات الجامعية والكتب والأبحاث باللغة العربية، وتحديد درجة التشابه أو أصالة الأعمال البحثية وحماية ملكيتها الفكرية. تعرف اكثر
![](/images/kashef-image.png)