摘要
介绍了区间时序逻辑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.
出处
《郑州大学学报（理学版）》
CAS
北大核心
2009年第4期31-34,44,共5页
Journal of Zhengzhou University:Natural Science Edition
基金
国家863高技术研究发展项目
编号2007AA010408
河南省重大科技攻关项目
编号092101210104
河南省教育厅自然科学研究项目
编号2006520015
2008A520024
关键词
区间时序逻辑
原型验证系统
辅助定理证明
interval temporal logic
prototype verification system
theorem proving
