Text Box:  

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

Integration Theory

Improper Integrals

Gamma Function


01save_logo (1)

 Higher-Order Logic Formalization of Gamma Function using Improper Integrals





System Analysis & Verification (SAVE) Lab, Seecs, NUST.