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

摘要：

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

关键词：出具证明编译器、自定义谓词、自动定理证明、推理规则

所属期刊栏目：34

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金项目61003043,61170018

在线出版日期：2013-11-05（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：1781-1786