概率论在Isabelle/HOL中的形式化

摘要：

基于测度论在Isabelle/HOL/Isar中形式化了概率论,给出了概率空间在Isabelle/HOL中的形式化定义,形式化验证了概率测度的主要性质。形式化验证了测度扩张定理,为在Isabelle/HOL中构造各种概率空间、形式化验证概率算法和概率系统奠定了基础。

关键词： 概率空间 测度扩张定理 形式化验证 测度论 概率测度 概率算法 概率系统

作者: 王金双 张兴元 张毓森

作者单位: 解放军理工大学指挥自动化学院 江苏南京 210007

会议类型: 国内会议

会议名称: 2007”信息与通信工程、电子科学与技术、计算机科学与技术、机械工程全国博士生学术论坛

会议地点: 西安

会议语种:中文

页码: 197-200

在线出版日期: 2007-09-15（万方平台首次上网日期，不代表论文的发表时间）