Formalization of Continuous Probability Distributions

12 years 7 days ago
Formalization of Continuous Probability Distributions
Continuous probability distributions are widely used to mathematically describe random phenomena in engineering and physical sciences. In this paper, we present a methodology that can be used to formalize any continuous random variable for which the inverse of the cumulative distribution function can be expressed in a closed mathematical form. Our methodology is primarily based on the Standard Uniform random variable, the classical cumulative distribution function properties and the Inverse Transform method. The paper includes the higher-orderlogic formalization details of these three components in the HOL theorem prover. To illustrate the practical effectiveness of the proposed methodology, we present the formalization of Exponential, Uniform, Rayleigh and Triangular random variables.
Osman Hasan, Sofiène Tahar
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2007
Where CADE
Authors Osman Hasan, Sofiène Tahar
Comments (0)