用于指针逻辑的自动定理证明器

摘要：

提出了一种为指针逻辑设计定理证明器的新技术,该项技术主要是基于变换和替代,已在APL的工具中得以实现.APL自动定理证明器是完全自动的,且其产生的证明可以被有效地记录和检验.已使用关于单链表、双链表和二叉树的指针程序测试了该自动定理证明器.

关键词：指针程序、指针逻辑、验证条件、自动定理证明器、证明检查器

所属期刊栏目：20

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

资助基金：the National Natural Science Foundation of China under Grant Nos.60673126, 90718026

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

页数：共14页

页码：2037-2050