Fractional calculus is a generalization of classical theories of integration and differentiation to arbitrary order (i.e., real or complex numbers). In the last two decades, this new paradigm has been widely used to model and analyze a wide class of physical systems in various fields of science and engineering. In this project, we plan to formalize the basic theory of fractional calculus in higher-order-logic. In particular, we require the the corresponding formalization of the Gamma function, Laplace transform, Z-transform and R-transform along with their important properties such as linearity and uniqueness, etc. In this project, we are using HOL Light theorem prover due to the availability of rich multivariate analysis libraries and some closely related projects about optics and signal processing. Our long term goal is to build the reasoning support which ultimately enable us to formally analysis wide class of fractional order systems, e.g., fractional order control, electromagnetics, signal processing and electrical networks.
Framework
People
Students
- Umair Siddique , PhD Candidate, HVG , Concordia University, QC, Canada
- Adnan Rashid , PhD Student, SAVe Lab , SEECS, NUST, Pakistan
Professors
- Osman Hasan , SEECS, NUST, Pakistan
- Sofiene Tahar , ECE Department, Concordia University, QC, Canada
Formalization in HOL
| Year | Topic | Contributors |
|---|---|---|
| 2015 -- Current | Finite Fractional Difference | Umair Siddique |
| 2014 -- Current | Inverse Z-Transform, Vectorial Z-transform | Umair Siddique and Sofiene Tahar |
| 2014 -- Current | Inverse Laplace Transform | Adnan Rashid and Osman Hasan |
| 2013 -- 2014 | Formalization of Z-Transform | Umair Siddique , Mohamed Yousri Mahmoud and Sofiene Tahar |
| 2012 -- 2013 | Formalization of Laplace Transform | Hira Taqdees and Osman Hasan |
| 2010 -- 2012 | Fractional Derivative and Integrals (real order) | Umair Siddique and Osman Hasan |
| 2010 -- 2011 | Improper Integrals, Gamma Function (real-valued) | Umair Siddique and Osman Hasan |
Publications
- U. Siddique and O. Hasan, On the Formalization of Gamma Function in HOL, Journal of Automated Reasoning (JAR), Vol. 53, No. 4, Springer, 2014, pp. 407-429
- U. Siddique, M. Y. Mahmoud and S. Tahar, On the Formalization of Z-Transform in HOL, Interactive Theorem Proving (ITP-14), Lecture Notes in Computer Science Volume 8558, 2014, Springer, pp. 483-498.
- S.H. Taqdees and O. Hasan, Formalization of Laplace Transform Using the Multivariate Calculus Theory of HOL-Light, Logic for Programing Artificial Intelligence and Reasoning (LPAR-13), Springer LNCS 8312, Stellenbosch, South Africa, pp. 744 – 758
- U. Siddique and O. Hasan “Analysis Techniques for Fractional Order Systems: A Survey ” in International Conference of Numerical Analysis and Applied Mathematics (ICNAAM-12), American Institute of Physics, Vol. 1479, 2012. pp 2106-2109
- U. Siddique and O. Hasan, “Formal Analysis of Fractional Order Systems in HOL“, Formal Methods in Computer Aided Design (FMCAD-11), IEEE, 2011. pp. 163- 170
- U. Siddique, “Formal analysis of Fractional Order Systems in Higher-order Logic “, Masters Thesis, National University of Sciences and Technology (NUST), Islamabad, Pakistan. August, 2011