基于PVS的ITL定理证明方法  

The Method for Proving ITL Theorem by Using PVS

作　　者：朱维军[1] 王迤冉[2] 周清雷[1] 

机构地区：[1]郑州大学信息工程学院,郑州450001 [2]周口师范学院计算机科学系,河南周口466001

出　　处：《郑州大学学报（理学版）》2009年第4期31-34,44,共5页Journal of Zhengzhou University:Natural Science Edition

基　　金：国家863高技术研究发展项目;编号2007AA010408;河南省重大科技攻关项目;编号092101210104;河南省教育厅自然科学研究项目;编号2006520015;2008A520024

摘　　要：介绍了区间时序逻辑ITL的语法、语义和公理系统以及通用的辅助定理证明工具PVS,研究了嵌入ITL到PVS的原理,给出了描述ITL的PVS模块,并给出一个实例,实现了基于PVS的ITL推理.在此基础上可以进一步实现基于PVS的多种扩展ITL推理.Syntax,semantics,axioms system of ITL,a verification tool for proving theorem with name of PVS are introduced.The method of inducing ITL theorem is discussed based on PVS and illustrated by example.A conclusion is drawn that EITL can be down with inducing based on PVS in the future work.

关 键 词：区间时序逻辑 原型验证系统 辅助定理证明 

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