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

Research of Automated Theorem Proving for User-defined Predicates

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

This paper adds user-defined predicate support in the assertion language to describe the property of the data structure, which enhances the expressivity of the assertion language based on a previous certifying compiler prototype. We design special inference rules, implements an automated theorem prover prototype for user-defined predicate using automated theorem proving techniques with- in the framework of the certifying compiler. Moreover, the prover is incorporated into the previous system. The prototype can prove the properties of the programs which operate on shared mutable data structures such as singly-linked lists, binary trees, etc., and the program specifications can use user-defined predicates to describe properties such as orderedness, length of the list and so on.