Abstract

In the field of probabilistic analysis, the concept of conditionalprobability plays a major role for estimating probabilities when some partial information concerning the result of the experiment is available. This paper presents ahigher-order-logic definition of conditionalprobability and the formal verification of some classical properties of conditionalprobability, such as, the total probability law and Bayes' theorem. This infrastructure, implemented in the HOL theoremprover, allows us to precisely reason about conditionalprobabilities for probabilistic systems within the sound core of HOL and thus proves to be quite useful for the analysis of systems used in safety-critical domains, such as space, medicine and transportation. To demonstrate the usefulness of our approach, we provide the precise probabilistic analysis of the binary asymmetric channel, a widely used concept in communication theory, within the HOL theoremprover.