I am Research Assistant at System
Analysis & Verification (SAVE) Lab, under the supervision of Dr. Osman Hasan. I also completed my Master’s thesis in the same lab
in 2011. |
The
Gamma function is a special transcendental function that is widely used
in probability theory, fractional calculus and analytical number theory.
This paper presents a higher-order logic formalization of the Gamma
function using the HOL theorem prover. Our formal definition of the Gamma
function is primarily based on the theory of improper integrals. The
contribution of this paper can be mainly divided into two parts.
Firstly, we formalize a general definition of an improper integral and
develop formal reasoning support for it by verifying some of its
classical properties. Secondly, we build upon these results to formalize
the Gamma function and verify some of its main properties, such as
pseudo-recurrence relation, functional equation and factorial
generalization. In order to illustrate the practical effectiveness and
utilization of our work, we formally verify some properties of Euler's
generalized power rule of differentiation, Mittag-Leffler functions, and
the relationship between the Exponential and Gamma random variables HOL Proof Scripts Higher-Order Logic Formalization
of Gamma Function using Improper Integrals |
Contact: System Analysis
& Verification (SAVE) Lab, Seecs, NUST. Umair.siddique@rcms.nust.edu.pk |