检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

投影时序逻辑的公理系统与形式验证

西安电子科技大学学报 2009年第4期36卷 680-685,729页

作者：舒新峰段振华西安电子科技大学计算理论与技术研究所陕西西安710071 西安邮电学院计算机系陕西西安710121

为了采用定理证明的方法对并发及交互式系统进行验证,提出了一阶投影时序逻辑的公理系统.利用投影时序逻辑既可描述待验证系统性质和规范,又可描述其实现模型的特点,在同一投影时序逻辑框架可以方便地对待验证系统进行建模和性质描述,... 详细信息

为了采用定理证明的方法对并发及交互式系统进行验证,提出了一阶投影时序逻辑的公理系统.利用投影时序逻辑既可描述待验证系统性质和规范,又可描述其实现模型的特点,在同一投影时序逻辑框架可以方便地对待验证系统进行建模和性质描述,并使用公理系统完成系统性质的证明.最后通过一个实例来展示投影时序逻辑及公理系统在系统验证中的应用.

关键词：投影时序逻辑公理系统形式化方法验证

基于模态逻辑D公理系统的Conformant规划方法

在线全文

学校读者我要写书评

暂无评论

计算机研究与发展 2009年第7期46卷 1160-1168页

作者：吕帅刘磊李莹石莲吉林大学计算机科学与技术学院长春130012 吉林大学符号计算与知识工程教育部重点实验室长春130012

2006年,conformant规划问题成为国际规划竞赛不确定性问题域中的标准测试问题,得到研究人员的广泛关注.目前,conformant规划系统都是将其看成信念状态空间上的启发式搜索问题予以求解.通过分析conformant规划问题的语法和语义,提出新的... 详细信息

2006年,conformant规划问题成为国际规划竞赛不确定性问题域中的标准测试问题,得到研究人员的广泛关注.目前,conformant规划系统都是将其看成信念状态空间上的启发式搜索问题予以求解.通过分析conformant规划问题的语法和语义,提出新的基于模态逻辑的规划框架,将其转换为模态逻辑D公理系统的一系列定理证明问题.提出2种基于模态逻辑的编码方式,构造相应的公理与推理规则形成模态公式集,保证对于D系统的定理证明过程等同于原问题的规划过程,并通过问题实例验证该方法的有效性.继基于SAT、CSP、线性规划、模型检测等求解技术的规划方法后,该规划框架是基于转换的规划方法的一种新的尝试.

关键词： conformant规划模态逻辑自动推理可满足性公理系统 D公理

在线全文

学校读者我要写书评

暂无评论

有穷时间投影时序逻辑的完备公理系统

软件学报 2011年第3期22卷 366-380页

作者：舒新峰段振华西安电子科技大学计算理论与技术研究所陕西西安710071 西安电子科技大学ISN国家重点实验室陕西西安710071 西安邮电学院计算机学院陕西西安710121

为采用定理证明的方法对并发及交互式系统进行验证,研究了有穷论域下有穷时间一阶投影时序逻辑(projection temporal logic,简称PTL)的一个完备公理系统.在介绍PTL的语法、语义并给出公理系统后,提出了PTL公式的正则形(normal form,简称... 详细信息

为采用定理证明的方法对并发及交互式系统进行验证,研究了有穷论域下有穷时间一阶投影时序逻辑(projection temporal logic,简称PTL)的一个完备公理系统.在介绍PTL的语法、语义并给出公理系统后,提出了PTL公式的正则形(normal form,简称NF)和正则图(normal form graph,简称NFG).基于NF给出了NFG的构造算法,并利用NFG可描述公式模型的性质证明PTL公式的可满足性判定定理和公理系统的完备性.最后,结合实例展示了PTL及其公理系统在系统验证中的应用.结果表明,基于PTL的定理证明方法可方便用于并发系统的建模与验证.

关键词：投影时序逻辑公理系统完备性证明定理证明形式化方法

具有模态词□φ=□_(1φ)∨□_(2φ)且可靠与完备的公理系统

在线全文

学校读者我要写书评

暂无评论

软件学报 2015年第9期26卷 2286-2296页

作者：邓少波黎敏曹存根眭跃飞中国科学院计算技术研究所智能信息处理重点实验室北京100190 中国科学院大学北京100049 南昌工程学院信息工程学院江西南昌330099

提出具有模态词□φ=□_(1φ)∨□_(2φ)的命题模态逻辑,给出其语言、语法与语义,其公理化系统是可靠与完备的,其中,□_1与□_2是给定的模态词.该逻辑的公理化系统具有与公理系统S5相似的语言,但具有不同的语法与语义.对于任意的公式φ... 详细信息

提出具有模态词□φ=□_(1φ)∨□_(2φ)的命题模态逻辑,给出其语言、语法与语义,其公理化系统是可靠与完备的,其中,□_1与□_2是给定的模态词.该逻辑的公理化系统具有与公理系统S5相似的语言,但具有不同的语法与语义.对于任意的公式φ,□φ=□_(1φ)∨□_(2φ);框架定义为三元组,模型定义为四元组;在完备性定理证明过程中,需要在由所有极大协调集所构成的集合上构造出两个等价关系,其典型模型的构建方法与经典典型模型的构建方法不同.如果□_1的可达关系R_1等于□_2的可达关系R_2,那么该逻辑的公理化系统变成S5.

关键词：命题模态逻辑模态词公理系统

在线全文

学校读者我要写书评

暂无评论

Pawlak粗糙集的公理系统

系统工程与电子技术 2006年第11期28卷 1752-1755页

作者：邱卫根广东工业大学计算机学院广东广州510090

粗糙集合理论是一种新的有效处理不精确、不确定、含糊信息的理论,粗集公理系统研究是粗集理论及应用研究的基础。利用模糊关系及其运算的矩阵表示,建立Pawlak粗近似空间的公理体系,该公理系统由三条相互独立的非常简洁的表达式构成。... 详细信息

粗糙集合理论是一种新的有效处理不精确、不确定、含糊信息的理论,粗集公理系统研究是粗集理论及应用研究的基础。利用模糊关系及其运算的矩阵表示,建立Pawlak粗近似空间的公理体系,该公理系统由三条相互独立的非常简洁的表达式构成。获得的结果深刻地揭示了经典等价关系与模糊等价关系的本质区别,进一步深化了Pawlak粗集理论。

关键词：粗糙集近似空间矩阵表示公理系统

Rasmusen智猪博弈公理系统与一类技术创新博弈

在线全文

学校读者我要写书评

暂无评论

系统工程学报 2013年第2期28卷 180-186页

作者：姜殿玉淮海工学院对策论及其应用研究所江苏连云港222005

为了定量地研究调整和控制"智猪"的劳动积极性问题,建立一门关于智猪博弈的严格、科学和系统的理论.基于Rasmusen智猪博弈模型,由公理化方法建立了智猪博弈公理系统.提出了Rasmusen技术创新博弈模型,举例说明了用本理论解决这类技术创... 详细信息

为了定量地研究调整和控制"智猪"的劳动积极性问题,建立一门关于智猪博弈的严格、科学和系统的理论.基于Rasmusen智猪博弈模型,由公理化方法建立了智猪博弈公理系统.提出了Rasmusen技术创新博弈模型,举例说明了用本理论解决这类技术创新问题的方法.结果表明,在小猪劳有其利的情况下,其劳动积极性高于大猪.由定量地调整和设置某些指标可调动和控制"智猪"的劳动积极性.

关键词：公理系统 Rasmusen智猪博弈 Rasmusen技术创新出食量槽板距跑速吃速