Sciweavers

JAR
2008

Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables

13 years 5 months ago
Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables
Statistical quantities, such as expectation (mean) and variance, play a vital role in the present age probabilistic analysis. In this paper, we present some formalization of expectation theory that can be used to verify the expectation and variance characteristics of discrete random variables within the HOL theorem prover. The motivation behind this is the ability to perform error free probabilistic analysis, which in turn can be very useful for the performance and reliability analysis of systems used in safety-critical domains, such as space travel, medicine and military. We first present a formal definition of expectation of a function of a discrete random variable. Building upon this definition, we formalize the mathematical concept of variance and verify some classical properties of expectation and variance in HOL. We then utilize these formal definitions to verify the expectation and variance characteristics of the Geometric random variable. In order to demonstrate the practical e...
Osman Hasan, Sofiène Tahar
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2008
Where JAR
Authors Osman Hasan, Sofiène Tahar
Comments (0)