首页> 中文期刊> 《计算机应用与软件》 >定理证明辅助工具Isabelle剖析与应用

定理证明辅助工具Isabelle剖析与应用

AI论文写作 >>

开具论文收录证明 >>

页面导航

摘要
著录项
引文网络
相似文献
相关主题

摘要

Isabelle是一个通用的定理证明器,应用领域广泛.介绍Isabelle逻辑系统的功能和构成,分析了Isabelle的规格说明语言、验证系统的特点,并给出了用Isabelle逻辑系统来构造Z规格说明的定理证明的方法.

著录项

来源
《计算机应用与软件》 |2007年第8期|14-16,43|共4页
作者
郭慧梅; 缪淮扣; 陈怡海;
展开▼
作者单位

上海大学计算机工程与科学学院;

上海;

200072;

上海大学计算机工程与科学学院;

上海;

200072;

上海大学计算机工程与科学学院;

上海;

200072;

展开▼
原文格式 PDF
正文语种 chi
中图分类计算技术、计算机技术;
关键词
逻辑系统; 定理证明器; 形式化方法;

相似文献

中文文献
外文文献
专利

1. 定理证明辅助工具PVS剖析 [J] . 廖宇 ,杨大军 . 计算机工程 . 2000,第009期
2. 基于Isabelle定理证明器算法程序的形式化验证 [J] . 游珍 ,薛锦云 . 计算机工程与科学 . 2009,第010期
3. 语料库与词典编纂的接口——词典编纂辅助工具Sketch Engine剖析 [J] . 陈国华 ,梁茂成 ,Adam . 广东外语外贸大学学报 . 2005,第B11期
4. Isabelle在分析安全操作系统状态机模型中的应用 [J] . 陈坤 ,贺也平 . 计算机工程与设计 . 2008,第003期
5. 骨科病人决策辅助工具的应用进展 [J] . 姚明鹤 ,娜飞沙·吐尔逊 ,张彦龙 . 护理研究 . 2021,第010期
6. 基于Isabelle定理证明器算法程序的形式化验证 [C] . 游珍 ,薛锦云 . 2009年全国理论计算机科学学术年会 . 2009
7. Isabelle定理证明器的剖析及其在PAR方法/PAR平台中的应用 [A] . 游珍 . 2009

获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

客服微信
服务号