Reasoning about conditional probabilities in a higher-order-logic theorem prover
type: Item
instance of: scholarly article
title: Reasoning about conditional probabilities in a higher-order-logic theorem prover
zbMATH Open document ID: 1216.68234
author: Osman Hasan
author: Sofiène Tahar
published in: Journal of Applied Logic
publication date: 2011-06-22T00:00:00Z
full work available at URL: reasoning about conditional probabilities.pdf
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68T37
zbMATH DE Number: 5911156
zbMATH Keywords: binary channel
zbMATH Keywords: Bayes theorem
zbMATH Keywords: formal methods
zbMATH Keywords: HOL theorem prover
zbMATH Keywords: probabilistic analysis
zbMATH Keywords: total probability law
describes a project that uses: Isabelle
describes a project that uses: ML
describes a project that uses: VESTA
describes a project that uses: HOL
MaRDI profile type: Publication
OpenAlex ID: W1972387650
cites work: Proofs of Randomized Algorithms in Coq
cites work: Q4813222
cites work: Q3998410
cites work: Q5679729
cites work: Q3723577
cites work: Q5287513
cites work: Q4231030
cites work: Formalization of Continuous Probability Distributions
cites work: Verification of Expectation Properties for Discrete Random Variables in HOL
cites work: Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function
cites work: Formal verification of tail distribution bounds in the HOL theorem prover
cites work: Performance analysis and functional verification of the stop-and-wait protocol in HOL
cites work: Q4484343
cites work: Verification of the Miller-Rabin probabilistic primality test.
cites work: Q4217794
cites work: A theory of type polymorphism in programming
cites work: Isabelle. A generic theorem prover
cites work: Q5687569
cites work: Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems
cites work: Q4664879
DOI: 10.1016/J.JAL.2011.01.001
description: scientific article; zbMATH DE number 5911156