定理证明辅助工具PVS剖析  

Analysis of Theorem-proving Aiding Tool──PVS

作　　者：廖宇[1] 杨大军[1] 

机构地区：[1]南京大学计算机科学与技术系,南京210093

出　　处：《计算机工程》2000年第9期140-142,共3页Computer Engineering

摘　　要：ＰＶＳ是斯坦福研究机构开发的强大的规约、验证系统，它的适用领域广泛。在概要介绍ＰＶＳ的构成、功能后，着重分析了ＰＶＳ的规约语言、验证系统的特点，以及使得ＰＶＳ灵活、强大的设计决策和内在机制．PVS is a powerful specification and verification system developed by Stanford Research Inshtute, its application area is broad. After briefly introducing the composition and function of PVS, this paper puts great emphasis on analyzing the features of PVS'specification language, verification system and design decisions, as well as inner mechanisms that make PVS powerful and flexible.

关 键 词：规约语言 定理证明器 PVS 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]