Using theorem proving to verify expectation and variance for discrete random variables

DOI10.1007/s10817-008-9113-6zbMath1191.68621OpenAlexW2115178223MaRDI QIDQ1040780

Osman Hasan, Sofiène Tahar

Publication date: 25 November 2009

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://spectrum.library.concordia.ca/974506/1/using_theorem_proving_to_verify_expectation.pdf

zbMATH Keywords

statistical propertiesprobabilistic analysisprobability theoryHOL theorem proverCoupon collector's problemhigher-order-logic

Mathematics Subject Classification ID

Related Items (4)

Formal probabilistic analysis of detection properties in wireless sensor networks ⋮ Formalization of Normal Random Variables in HOL ⋮ Formalization of Shannon's theorems ⋮ On the formalization of gamma function in HOL

Uses Software

• ML
• VESTA
• HOL
• VESTA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A theory of type polymorphism in programming
• Probabilistic guarded commands mechanized in HOL
• Verification of Expectation Properties for Discrete Random Variables in HOL
• A stochastic process on the hypercube with applications to peer-to-peer networks
• Formalization of Continuous Probability Distributions
• Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function
• Proofs of Randomized Algorithms in Coq
• Coalescing times for IID random variables with applications to population biology
• Keplers komplizierter Weg zur Wahrheit: Von neuen Schwierigkeiten, die „Astronomia Nova”︁ zu lesen
• Elementary Probability
• Theoretical Aspects of Computing – ICTAC 2005
• Probability and Computing
• Theorem Proving in Higher Order Logics
• Automata, Languages and Programming
• A formulation of the simple theory of types

This page was built for publication: Using theorem proving to verify expectation and variance for discrete random variables