支持用户自定义谓词的自动定理证明的研究

• 作者: 李兆鹏 汪娟 陈意云
• 来源期刊: 小型微型计算机系统
• 学科: 工学
• 关键词: 出具证明编译器 自定义谓词 自动定理证明 推理规则
• 年，卷（期）: 2013,（8）
• 所属期刊栏目: 计算机软件与数据库
• 页码范围: 1781-1786
• 页数: 6页
• 分类号: TP311
• 字数: 8999字
• 语种: 中文

摘要

在先前设计的一个出具证明编译器原型基础上,增加了可用来描述数据结构性质的自定义谓词,对断言语言表达能力方面做了提升.在出具证明编译器的框架内,借助自动定理证明技术,针对自定义谓词的特点,设计了专门的推理规则,由此实现自定义谓词专用的自动定理证明器原型,并将它并入系统原来的自动定理证明器中.该原型可以用来证明操作单链表、二叉树等共享数据结构的程序的性质,其程序规范中可以使用自定义谓词描述数据有序性、链表长度等性质.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈意云	中国科学技术大学计算机科学与技术学院	83	854	16.0	26.0
5	李兆鹏	中国科学技术大学计算机科学与技术学院	17	99	7.0	9.0
9	汪娟	中国科学技术大学计算机科学与技术学院	1	1	1.0	1.0