Reasoning about conditional probabilities in a higher-order-logic theorem prover
From MaRDI portal
Publication:545151
DOI10.1016/j.jal.2011.01.001zbMath1216.68234OpenAlexW1972387650MaRDI QIDQ545151
Publication date: 22 June 2011
Published in: Journal of Applied Logic (Search for Journal in Brave)
Full work available at URL: https://spectrum.library.concordia.ca/974505/1/reasoning_about_conditional_probabilities.pdf
probabilistic analysisformal methodsBayes theorembinary channelHOL theorem provertotal probability law
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Performance analysis and functional verification of the stop-and-wait protocol in HOL
- A theory of type polymorphism in programming
- Isabelle. A generic theorem prover
- Verification of the Miller-Rabin probabilistic primality test.
- Verification of Expectation Properties for Discrete Random Variables in HOL
- Formal verification of tail distribution bounds in the HOL theorem prover
- Formalization of Continuous Probability Distributions
- Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function
- Proofs of Randomized Algorithms in Coq
- Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems