Login | Register

Reasoning about conditional probabilities in a higher-order-logic theorem prover

Title:

Reasoning about conditional probabilities in a higher-order-logic theorem prover

Hasan, Osman and Tahar, Sofiène (2011) Reasoning about conditional probabilities in a higher-order-logic theorem prover. Journal of Applied Logic, 9 (1). pp. 23-40. ISSN 15708683

[thumbnail of reasoning_about_conditional_probabilities.pdf]
Preview
Text (application/pdf)
reasoning_about_conditional_probabilities.pdf - Accepted Version
174kB

Official URL: http://dx.doi.org/10.1016/j.jal.2011.01.001

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.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Article
Refereed:Yes
Authors:Hasan, Osman and Tahar, Sofiène
Journal or Publication:Journal of Applied Logic
Date:2011
Digital Object Identifier (DOI):10.1016/j.jal.2011.01.001
ID Code:974505
Deposited By: ANDREA MURRAY
Deposited On:31 Jul 2012 20:19
Last Modified:18 Jan 2018 17:38
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top