Formalization of Continuous Probability Distributions
Formalization of Continuous Probability Distributions
复制标题
连续概率分布的形式化
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
S. Tahar
中科院分区：
文献类型：
--
作者：
O. Hasan;S. Tahar
在工程和物理科学中，连续概率分布被广泛用于数学描述随机现象。在这篇文章中，我们提出了一种方法，可以用来形式化任何连续的随机变量，对其累积分布函数的逆可以用封闭的数学形式表示。我们的方法主要是基于标准均匀随机变量、经典累积分布函数性质和逆变换方法。文中给出了HOL定理证明器中这三个部分的高阶逻辑形式化细节。为了说明该方法的实际有效性，我们给出了指数随机变量、均匀随机变量、瑞利随机变量和三角随机变量的形式化。
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-order-logic 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.