检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

集值信息系统的公理系统

逻辑学研究 2022年第5期15卷 51-69页

作者：曹发生贵州民族大学民族文化与认知科学学院

自从波兰数学家Z.Pawlak建立信息表的逻辑系统以来,出现了各种信息系统及其逻辑的研究。集值信息系统在机器学习方面有着重要的应用,本文从一个具体的集值信息系统的例子引发出建立集值信息系统的公理系统必要性。首先借助相容性关系给... 详细信息

自从波兰数学家Z.Pawlak建立信息表的逻辑系统以来,出现了各种信息系统及其逻辑的研究。集值信息系统在机器学习方面有着重要的应用,本文从一个具体的集值信息系统的例子引发出建立集值信息系统的公理系统必要性。首先借助相容性关系给出模态算子的语义;然后给出集值信息系统的逻辑的语法和语义;最后建立集值信息系统的公理系统的公理和推理规则,并且利用传统方法证明集值信息系统的逻辑系统的可靠性和完全性。从逻辑本质上看,集值信息系统的逻辑系统就是一种多模态逻辑系统,它也给出多模态逻辑的非常完美的诠释。

关键词：集值信息系统过滤典范模型公理系统

具有模态词□φ=□_(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.

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

在线全文

学校读者我要写书评

暂无评论

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

软件学报 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的定理证明方法可方便用于并发系统的建模与验证.

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

在线全文

学校读者我要写书评

暂无评论

MSVL语言的公理系统的程序验证

西安电子科技大学学报 2010年第1期37卷 96-101页

作者：杨潇潇段振华西安电子科技大学计算理论与技术研究所陕西西安710071

MSVL语言是一种用于模拟、建模和验证程序的区间时序逻辑程序设计语言.为了证明区间时序逻辑程序的正确性,提出了MSVL语言的一个公理系统:包括正则形转换的状态公理和状态推演规则,以及将程序从一个状态转换到另一个状态的区间公理和区... 详细信息

MSVL语言是一种用于模拟、建模和验证程序的区间时序逻辑程序设计语言.为了证明区间时序逻辑程序的正确性,提出了MSVL语言的一个公理系统:包括正则形转换的状态公理和状态推演规则,以及将程序从一个状态转换到另一个状态的区间公理和区间推演规则.最后给出验证实例说明基于该公理系统的程序验证方法.

关键词：形式验证时序逻辑正则形安全性公理系统

在线全文

学校读者我要写书评

暂无评论

任意公理系统的依赖基

计算机科学 2013年第2期40卷 200-205页

作者：马垣辽宁科技大学软件学院鞍山114051

形式化定义了值依赖的公理、公理系统及依赖基。严格证明了任何公理系统对任何背景都具有依赖基,给出了对任意一个公理系统求任意背景依赖基的方法,并证明了每个公理系统的依赖基不唯一。进而还提出了一种诱导背景,通过诱导背景可把这... 详细信息

形式化定义了值依赖的公理、公理系统及依赖基。严格证明了任何公理系统对任何背景都具有依赖基,给出了对任意一个公理系统求任意背景依赖基的方法,并证明了每个公理系统的依赖基不唯一。进而还提出了一种诱导背景,通过诱导背景可把这个证明过程及依赖基的计算过程形象地反映出来。

关键词：值依赖公理系统依赖基诱导背景

在线全文

学校读者我要写书评

暂无评论

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

西安电子科技大学学报 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公理

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

在线全文

学校读者我要写书评

暂无评论

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

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

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

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

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

模态逻辑GL的基于广义谢弗竖的分析性模态公理系统(英文)

在线全文

学校读者我要写书评

暂无评论

逻辑学研究 2016年第2期9卷 1-13页

作者：唐芳芳中国社会科学院马克思主义研究院

基于广义谢弗竖这种新算子,本文构造了模态逻辑GL的模态表列和分析性模态公理系统。广义谢弗竖是一种n元算子,为模态逻辑的表达式提供一种新记法,使分析性模态公理系统的陈述直接明了。由于谢弗竖是一种新算子,基于它的模态表列规则与... 详细信息

基于广义谢弗竖这种新算子,本文构造了模态逻辑GL的模态表列和分析性模态公理系统。广义谢弗竖是一种n元算子,为模态逻辑的表达式提供一种新记法,使分析性模态公理系统的陈述直接明了。由于谢弗竖是一种新算子,基于它的模态表列规则与通常的基于模态词和联结词的表列规则有所不同。分析性模态公理系统中的内定理证明很简单。因为分析性模态公理系统与模态表列之间存在某种对应关系,所以GL的分析性模态公理系统的完全性由GL的模态表列的完全性结果易证。GL的模态系统的完全性证明比较特殊,无法直接应用证明模态逻辑完全性的一般方法——典范模型方法,需要用一种过滤的方法挑出一些可能世界构造有穷模型。

关键词：模态逻辑分析性 GL 公理系统完全性 inferential 记法 frames 定理证明 branch