nach oben

Erschienen in:

2015 | OriginalPaper | Buchkapitel

Towards the Formalization of Fractional Calculus in Higher-Order Logic

verfasst von : Umair Siddique, Osman Hasan, Sofiène Tahar

Erschienen in: Intelligent Computer Mathematics

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

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 mathematical modeling approach has been widely used toanalyze a wide class of physical systems in various fields of science and engineering. In this paper, we describe an ongoing project which aims at formalizing the basic theories of fractional calculus in the HOL Light theorem prover. Mainly, we present the motivation and application of such formalization efforts, a roadmap to achieve our goals, current status of the project and future milestones.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel A Survey on Retrieval of Mathematical Knowledge

Nächstes Kapitel LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners

http://save.seecs.nust.edu.pk/projects/fc.html.

http://save.seecs.nust.edu.pk.

https://code.google.com/p/hol-light/source/browse/trunk/Multivariate/gamma.ml.

Pariz, N., Kiani-B, A., Fallahi, K., Leung, H.: A Chaotic secure communication scheme using fractional chaotic systems based on an extended fractional kalman filter. Commun. Nonlinear Sci. Numer. Simul. 14, 863–879 (2009)MathSciNetCrossRefMATH

Afshar, S.K., Siddique, U., Mahmoud, M.Y., Aravantinos, V., Seddiki, O., Hasan, O., Tahar, S.: Formal analysis of optical systems. Math. Comput. Sci. 8(1), 39–70 (2014)MathSciNetCrossRefMATH

Atici, F.M.: A transform method in discrete fractional calculus. Int. J. Diff. Equ. 2(2), 165–176 (2007)MathSciNet

Atici, F.M., Eloe, P.W.: Initial value problems in discrete fractional calculus. Proc. Am. Math. Soc. 137(3), 981–989 (2009)MathSciNetCrossRefMATH

Auastasio, T.J.: The fractional-order dynamics of brainstem vestibulo-oculomotor neurons. Biol. Cybern. 72(1), 69–79 (1994)CrossRef

Cuestab, E., Quintanoa, C.: Improving satellite image classification by using fractional type convolution filtering. Int. J. Appl. Earth Obs. Geoinf. 12(4), 298–301 (2010)CrossRef

Chen, Y.Q., Xue, D., Dou, H.: Fractional calculus and biomimetic control. In: Robotics and Biomimetics, pp. 901–906. IEEE (2004)

Marín, M., Domínguez, D.M., Camacho, M.: Macrophage ion currents are fit by a fractional model and therefore are a time series with memory. Eur. Biophys. J. 38(4), 457–464 (2009)CrossRef

Dalir, M., Bashour, M.: Application of fractional calculus. Appl. Frac. Calc. Phys. 4(21), 12 (2010)MathSciNetMATH

10.

Das, S.: Functional Fractional Calculus for System Identification and Controls. Springer, Heidelberg (2007)

11.

Duarte, F.B.M., Machado, J.A.T.: Pseudoinverse trajectory control of redundant manipulators: a fractional calculus perspective. In: International Conference on Robotics and Automation, pp. 2406–2411. IEEE (2002)

12.

Elaydi, S.: An Introduction to Difference Equations. Springer, New York (2005)MATH

13.

Engheta, N.: Fractional curl operator in electromagnetics. Microw. Opt. Technol. Lett. 17(2), 86–91 (1998)CrossRef

14.

Faryad, M., Naqvi, Q.A.: Fractional rectangular waveguide. Progr. Electromagn. Res. PIER 75, 383–396 (2007)CrossRef

15.

Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le Roux, S., Mahboubi, A., O’Connor, R., Ould Biha, S., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Théry, L.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 163–179. Springer, Heidelberg (2013) CrossRef

16.

Hales, T.C.: Introduction to the Flyspeck project. In: Mathematics, Algorithms, Proofs, volume 05021 of Dagstuhl Seminar Proceedings, pp. 1–11 (2005)

17.

Hartley, T.T., Lorenzo, C.F.: Fractional system identification: an approach using continuous order distributions. Technical report, National Aeronautics and Space Administration, Glenn Research Cente NASA TM (1999)

18.

Ahmad, W.M., Assaleh, K.: Modeling of speech signals using fractional calculus. In: International Symposium on Signal Processing and Its Applications, pp. 1–4. IEEE (2007)

19.

Krishna, B.T., Reddy, K.V.V.S.: Design of digital differentiators and integrators of order \(\frac{1}{2}\). World J. Model. Simul. 4, 182–187 (2008)

20.

Leibnitz, G.W.: Leibnitzens Mathematische Schriften. SIGDA News Lett. 2, 301–302 (1962)

21.

Lurie, K.A.: An Introduction to the Mathematical Theory of Dynamic Materials. Springer, US (2007)MATH

22.

Magin, R.L.: Fractional calculus models of complex dynamics in biological tissues. Comput. Math. Appl. 59, 1586–1593 (2010)MathSciNetCrossRefMATH

23.

Maione, G., Lino, P.: New tuning rules for fractional \(pi^{\alpha }\) controllers. Nonlinear Dyn. 49(1–2), 251–257 (2007)CrossRefMATH

24.

Miller, K.S., Ross, B.: An Introduction to Fractional Calculus and Fractional Differential Equations. Willey, New York (1993)MATH

25.

Naqvi, Q.A., Abbas, M.: Complex and higher order fractional curl operator in electromagnetics. Opt. Commun. 241, 349–355 (2004)CrossRef

26.

Ogata, K.: Modern Control Engineering. Prentice Hall, Boston (2010)MATH

27.

Oldham, K.B., Spanier, J.: The Fractional Calculus. Academic Press, New York (1974)MATH

28.

Oppenheim, A.V., Schafer, R.W., Buck, J.R.: Discrete-Time Signal Processing. Prentice Hall, Upper Saddle River (1999)

29.

Mathieu, B., Melchior, P., Oustaloup, A., Ceyral, C.: Fractional differentiation for edge detection. Signal Process. 83, 2421–2432 (2003)CrossRefMATH

30.

Petrás, I., Vinagre, B.M.: Practical application of digital fractional-order controller to temperature control. Acta Montan. Slovaca 7(2), 131–137 (2002)

31.

Podlubny, I.: Fractional Differential Equations. Academic Press, New York (1999)MATH

32.

Ross, B.: A brief history and exposition of the fundamental theory of fractional calculus. In: Ross, B. (ed.) Fractional Calculus and Its Applications. Lecture Notes in Mathematics, vol. 457, pp. 1–36. Springer, Heidelberg (1975)CrossRef

33.

Siddique, U., Hasan, O.: Formal analysis of fractional order systems in HOL. In: Formal Methods in Computer Aided Design, pp. 163–170. IEEE (2011)

34.

Siddique, U., Hasan, O.: On the formalization of gamma function in HOL. J. Autom. Reason. 53(4), 407–429 (2014)MathSciNetCrossRefMATH

35.

Siddique, U., Mahmoud, M.Y., Tahar, S.: On the formalization of Z-Transform in HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 483–498. Springer, Heidelberg (2014)

36.

Taqdees, S.H., Hasan, O.: Formalization of laplace transform using the multivariable calculus theory of HOL-light. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 744–758. Springer, Heidelberg (2013) CrossRef

37.

Tseng, C.C.: Design of fractional order digital FIR differentiators. IEEE Signal Process. Lett. 8(3), 77–79 (2001)MathSciNetCrossRef

38.

Vinagreb, B.M., Chena, Y.Q.: Fractional differentiation for edge detection. Signal Process. 83, 2359–2365 (2003)CrossRef

39.

Yang, X.S.: Mathematical Modeling with Multidisciplinary Applications. Wiley, New Jersey (2013) CrossRefMATH

40.

Zaborovsky, V., Meylanov, R.: Informational network traffic model based on fractional calculus. In: Proceedings of the International Conference Info-tech and Info-net, pp. 58–63. IEEE (2001)

Titel: Towards the Formalization of Fractional Calculus in Higher-Order Logic
verfasst von: Umair Siddique
Osman Hasan
Sofiène Tahar
Verlag: Springer International Publishing
Buch: Intelligent Computer Mathematics
Print ISBN: 978-3-319-20614-1

Electronic ISBN: 978-3-319-20615-8

Copyright-Jahr: 2015
DOI: https://doi.org/10.1007/978-3-319-20615-8_21

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner