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

DOI10.1016/j.jal.2011.01.001zbMath1216.68234OpenAlexW1972387650MaRDI QIDQ545151

Osman Hasan, Sofiène Tahar

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

zbMATH Keywords

probabilistic analysisformal methodsBayes theorembinary channelHOL theorem provertotal probability law

Mathematics Subject Classification ID

Reasoning under uncertainty in the context of artificial intelligence (68T37)

Related Items

Formal reasoning about finite-state discrete-time Markov chains in HOL

Uses Software

• Isabelle
• ML
• HOL
• VESTA

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item