Formalization of transform methods using HOL Light

DOI10.1007/978-3-319-62075-6_22zbMath1367.68255arXiv1705.10050OpenAlexW2618528743MaRDI QIDQ2364690

Osman Hasan, Adnan Rashid

Publication date: 21 July 2017

Full work available at URL: https://arxiv.org/abs/1705.10050

zbMATH Keywords

Fourier transformLaplace transforminteractive theorem provingHOL Light

Mathematics Subject Classification ID

Software, source code, etc. for problems pertaining to integral transforms (44-04) Software, source code, etc. for problems pertaining to harmonic analysis on Euclidean spaces (42-04)

Related Items

Formal analysis of continuous-time systems using Fourier transform ⋮ On the formalization of the heat conduction problem in HOL

Uses Software

• ACL2
• HOL Light
• GitHub

Cites Work

• Markov dilations and quantum detailed balance
• On the Formalization of Fourier Transform in Higher-order Logic
• Formalization of Laplace Transform Using the Multivariable Calculus Theory of HOL-Light
• On the Formalization of Z-Transform in HOL
• Trivector Fourier transformation and electromagnetic field
• Formal Methods in Computer-Aided Design
• The correctness of the fast Fourier transform: A structured proof in ACL2
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Formalization of transform methods using HOL Light