You are previewing Formalized Probability Theory and Applications Using Theorem Proving.
O'Reilly logo
Formalized Probability Theory and Applications Using Theorem Proving

Book Description

Scientists and engineers often have to deal with systems that exhibit random or unpredictable elements and must effectively evaluate probabilities in each situation. Computer simulations, while the traditional tool used to solve such problems, are limited in the scale and complexity of the problems they can solve. Formalized Probability Theory and Applications Using Theorem Proving discusses some of the limitations inherent in computer systems when applied to problems of probabilistic analysis, and presents a novel solution to these limitations, combining higher-order logic with computer-based theorem proving. Combining practical application with theoretical discussion, this book is an important reference tool for mathematicians, scientists, engineers, and researchers in all STEM fields.

Table of Contents

  1. Cover
  2. Title Page
  3. Copyright Page
  4. Dedication
  5. Preface
  6. Acknowledgment
  7. Chapter 1: Probabilistic Analysis
    1. ABSTRACT
    2. 1.1 MOTIVATION
    3. 1.2 RANDOMIZED MODELS
    4. 1.3 PROBABILISTIC PROPERTIES
    5. 1.4 STATISTICAL PROPERTIES
    6. 1.5 TRADITIONAL PROBABILISTIC ANALYSIS METHODS
    7. 1.6 CONCLUSION
    8. REFERENCES
    9. KEY TERMS AND DEFINITIONS
  8. Chapter 2: Formal Verification Methods
    1. ABSTRACT
    2. 2.1 INTRODUCTION
    3. 2.2 MODEL CHECKING
    4. 2.3 THEOREM PROVING
    5. 2.4 CONCLUSION
    6. REFERENCES
    7. KEY TERMS AND DEFINITIONS
  9. Chapter 3: Probabilistic Analysis Using Theorem Proving
    1. ABSTRACT
    2. 3.1 METHODOLOGY
    3. 3.2 HOL4 THEOREM PROVER
    4. 3.3 CONCLUSION
    5. REFERENCES
    6. KEY TERMS AND DEFINITIONS
  10. Chapter 4: Measure Theory and Lebesgue Integration Theories
    1. ABSTRACT
    2. 4.1 FORMALIZATION OF EXTENDED REAL NUMBERS
    3. 4.2 FORMALIZATION OF MEASURE THEORY
    4. 4.3 FORMALIZATION OF LEBESGUE INTEGRATION IN HOL
    5. 4.4 CONCLUSION
    6. REFERENCES
    7. KEY TERMS AND DEFINITIONS
  11. Chapter 5: Probability Theory
    1. ABSTRACT
    2. 5.1 FORMALIZATION OF PROBABILITY THEORY
    3. 5.2 FORMALIZATION OF STATISTICAL PROPERTIES
    4. 5.3 HEAVY HITTER PROBLEM
    5. 5.4 FORMALIZATION OF CONDITIONAL PROBABILITIES
    6. 5.5 CONCLUSION
    7. REFERENCES
    8. KEY TERMS AND DEFINITIONS
  12. Chapter 6: Discrete-Time Markov Chains in HOL
    1. ABSTRACT
    2. 6.1 FORMALIZATION OF DISCRETE-TIME MARKOV CHAIN
    3. 6.2 FORMAL VERIFICATION DTMC PROPERTIES
    4. 6.3 FORMALIZATION OF STATIONARY DISTRIBUTIONS
    5. 6.4 FORMALIZATION OF STATIONARY PROCESS
    6. 6.5 BINARY COMMUNICATION MODEL
    7. 6.6 AMQM PROTOCOL
    8. 6.7 CONCLUSION
    9. REFERENCES
    10. KEY TERMS AND DEFINITIONS
  13. Chapter 7: Classified Discrete-Time Markov Chains
    1. ABSTRACT
    2. 7.1 FORMALIZATION OF CLASSIFIED STATES
    3. 7.2 FORMALIZATION OF CLASSIFIED DTMCs
    4. 7.3 FORMAL VERIFICATION OF LONG-TERM PROPERTIES
    5. 7.4 APPLICATIONS
    6. 7.5 CONCLUSION
    7. REFERENCES
    8. KEY TERMS AND DEFINITIONS
  14. Chapter 8: Formalization of Hidden Markov Model
    1. ABSTRACT
    2. 8.1 DEFINITION OF HMM
    3. 8.2 HMM PROPERTIES
    4. 8.3 PROOF AUTOMATION
    5. 8.4 APPLICATION: DNA SEQUENCE ANALYSIS
    6. 8.5 CONCLUSION
    7. REFERENCES
    8. KEY TERMS AND DEFINITIONS
  15. Chapter 9: Information Measures
    1. ABSTRACT
    2. 9.1 FORMALIZATION OF RADON-NIKODYM DERIVATIVE
    3. 9.2 FORMALIZATION OF KULLBACK-LEIBLER DIVERGENCE
    4. 9.3 FORMALIZATION OF MUTUAL INFORMATION
    5. 9.4 ENTROPY
    6. 9.5 FORMALIZATION OF CONDITIONAL MUTUAL INFORMATION
    7. 9.6 FORMALIZATION OF QUANTITATIVE ANALYSIS OF INFORMATION
    8. 9.7 CONCLUSION
    9. REFERENCES
    10. KEY TERMS AND DEFINITIONS
  16. Chapter 10: Formal Analysis of Information Flow Using Min-Entropy and Belief Min-Entropy
    1. ABSTRACT
    2. 10.1 INFORMATION FLOW ANALYSIS
    3. 10.2 FORMALIZATION OF MIN-ENTROPY AND BELIEF MIN-ENTROPY
    4. 10.3 FORMAL ANALYSIS OF INFORMATION FLOW
    5. 10.4 APPLICATION: CHANNELS IN CASCADE
    6. 10.5 CONCLUSION
    7. REFERENCES
    8. KEY TERMS AND DEFINITIONS
  17. Chapter 11: Applications of Formalized Information Theory
    1. ABSTRACT
    2. 11.1 DATA COMPRESSION
    3. 11.2 ANONYMITY-BASED SINGLE MIX
    4. 11.3 ONE-TIME PAD
    5. 11.4 CONCLUSION
    6. REFERENCES
    7. KEY TERMS AND DEFINITIONS
  18. Chapter 12: Reliability Theory
    1. ABSTRACT
    2. 12.1 LIFETIME DISTRIBUTIONS
    3. 12.2 CUMULATIVE DISTRIBUTION FUNCTION
    4. 12.3 SURVIVAL FUNCTION
    5. 12.4 RELIABILITY BLOCK DIAGRAMS
    6. 12.5 APPLICATIONS
    7. 12.6 CONCLUSION
    8. REFERENCES
    9. KEY TERMS AND DEFINITIONS
  19. Chapter 13: Scheduling Algorithm for Wireless Sensor Networks
    1. ABSTRACT
    2. 13.1 COVERAGE-BASED RANDOMIZED SCHEDULING ALGORITHM
    3. 13.2 FORMAL ANALYSIS OF THE K-SET RANDOMIZED SCHEDULING
    4. 13.3 FORMAL ANALYSIS OF WSN FOR FOREST FIRE DETECTION
    5. 13.4 CONCLUSION
    6. REFERENCES
    7. KEY TERMS AND DEFINITIONS
  20. Chapter 14: Formal Probabilistic Analysis of Detection Properties in Wireless Sensor Networks
    1. ABSTRACT
    2. 14.1 DETECTION OF A WIRELESS SENSOR NETWORK
    3. 14.2 DETECTION PROPERTIES
    4. 14.3 WSN FOR BORDER SURVEILLANCE
    5. 14.4 CONCLUSION
    6. REFERENCES
    7. KEY TERMS AND DEFINITIONS
  21. Conclusion
    1. 1. SUMMARY
    2. 2. FUTURE DIRECTIONS
  22. Related References
  23. Compilation of References
  24. About the Authors