On the formalization of gamma function in HOL

DOI10.1007/s10817-014-9311-3zbMath1315.68224OpenAlexW2137545064MaRDI QIDQ2352499

Umair Siddique, Osman Hasan

Publication date: 2 July 2015

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-014-9311-3

zbMATH Keywords

gamma functionMittag-Leffler functionfractional calculusgamma random variable

Mathematics Subject Classification ID

Related Items (4)

Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm ⋮ Formal proofs of hypergeometric sums. Dedicated to the memory of Andrzej Trybulec ⋮ Towards the Formalization of Fractional Calculus in Higher-Order Logic ⋮ Formalization of fractional order PD control systems in HOL4

Uses Software

• Mathematica
• Matlab
• ML
• Isabelle/HOL
• PVS
• HOL
• HOL Light

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Mittag-Leffler functions and their applications
• Computer theorem proving in mathematics
• Fractional differentiation for edge detection
• Fractional calculus models of complex dynamics in biological tissues
• Using theorem proving to verify expectation and variance for discrete random variables
• A theory of type polymorphism in programming
• The HOL Light theory of Euclidean space
• Three Chapters of Measure Theory in Isabelle/HOL
• Modeling the Cardiac Tissue Electrode Interface Using Fractional Calculus
• Formalization of Finite-State Discrete-Time Markov Chains in HOL
• A Brief Overview of HOL4
• Formalization of Continuous Probability Distributions
• On Kronecker limit formula for real quadratic fields
• On the Formalization of the Lebesgue Integration Theory in HOL

This page was built for publication: On the formalization of gamma function in HOL