检索结果-内蒙古大学图书馆

西南交通大学学报 2025年第1期60卷 185-193页

作者：曾国艳徐扬陈树伟姜世攀西南交通大学数学学院四川成都611756 西南交通大学系统可信性自动验证国家地方联合工程实验室四川成都611756

基于一阶逻辑的自动定理证明器(ATP)在知识表达和自动推理研究中占据重要地位,而启发式策略则是提升ATP性能的关键研究方向.主流的启发式策略通常通过描述子句属性来确定属性优先级,从而选择子句,但属性优先级受人为因素影响,且评估子... 详细信息

基于一阶逻辑的自动定理证明器(ATP)在知识表达和自动推理研究中占据重要地位,而启发式策略则是提升ATP性能的关键研究方向.主流的启发式策略通常通过描述子句属性来确定属性优先级,从而选择子句,但属性优先级受人为因素影响,且评估子句耗时较长.为此,本文基于矛盾体分离(S-CS)规则,提出一种新的多属性决策(MCDM)子句评估方法.首先,利用熵权法对子句属性进行客观赋权;其次,结合偏好顺序结构评估法(PROMETHEEⅡ)对子句进行评估,得到子句的完全排序;最后,将提出的MCDM方法加入自动定理证明器CSE 1.5(contradiction separation extension 1.5)、Vampire 4.7和Eprover(E 2.6)中,分别形成新的证明器MCDM_CSE、MCDM_V和MCDM_E.对MCDM_CSE测试了国际定理证明器问题库TPTP(Thousands of Problems for Theorem Provers)中一阶逻辑格式的定理,并对MCDM_V和MCDM_E测试了2022年CADE(Conference on Automated Deduction)竞赛例(一阶逻辑组).实验表明:MCDM_CSE比CSE 1.5多证明了151个定理(来自TPTP),并且能够证明Vampire 4.7无法证明的5个定理、E 2.6无法证明的41个定理以及Prover9无法证明的293个定理;在更短的平均时间内,MCDM_V比Vampire 4.7多证明了6个定理(来自CADE 2022),MCDM_E比E 2.6多证明了8个定理.

关键词：一阶逻辑矛盾体分离规则启发式策略多属性决策熵权法

来源：评论

学校读者我要写书评

暂无评论

一种基于新型混淆操作的RFID双向认证协议

引用

计算机工程与科学 2025年第2期47卷 247-255页

作者：贾昊洲徐鹏王丹琛徐扬系统可信性自动验证国家地方联合工程实验室西南交通大学数学学院四川省数字经济研究中心

针对RFID系统中存在的隐私和安全问题，提出了一种基于新型混淆操作的超轻量RFID认证协议，通过利用简单的逐位异或、循环左旋转和新提出的超轻量化分组循环操作，达到低复杂度、高安全性的目的。此外，由于在协议交互过程中的消息根据... 详细信息

针对RFID系统中存在的隐私和安全问题，提出了一种基于新型混淆操作的超轻量RFID认证协议，通过利用简单的逐位异或、循环左旋转和新提出的超轻量化分组循环操作，达到低复杂度、高安全性的目的。此外，由于在协议交互过程中的消息根据随机数生成，攻击者无法通过穷举来破解消息。分析与验证结果表明，所提协议可以有效地抵御常见的网络攻击类型，并且在计算和存储成本方面具备优势。

关键词： RFID认证协议混淆操作分组循环操作形式化验证

来源：评论

学校读者我要写书评

暂无评论

一种车联网V2V认证与密钥交换协议设计与验证

引用

信息安全研究 2025年第5期 465-472页

作者：王秀珍徐鹏陈美荣王丹琛徐扬系统可信性自动验证国家地方联合工程实验室西南交通大学数学学院成都纺织高等专科学校四川省数字经济研究中心

车联网系统中，车辆行驶过程需与其他车辆通信以实现信息交换，要求必须具备高安全、低延迟、用户匿名性等安全特性.认证与密钥交换协议以密码算法为基础旨在完成会话密钥协商，用于通信双方后续信息交换，是保证车联网通信安全的重要手... 详细信息

车联网系统中，车辆行驶过程需与其他车辆通信以实现信息交换，要求必须具备高安全、低延迟、用户匿名性等安全特性.认证与密钥交换协议以密码算法为基础旨在完成会话密钥协商，用于通信双方后续信息交换，是保证车联网通信安全的重要手段.现有协议注册阶段需在线下安全信道中进行，与实际不符，且认证阶段多基于第三方并需多轮信息交互，增加了过程复杂度.因此设计了一种基于公共信道的V2V(vehicle to vehicle)协议，协议交互过程不需依赖第三方，仅需进行2轮信息交换，同时添加快速登录阶段以解决网络突然中断造成的信息交换延迟问题，理论分析与形式化验证结果表明协议满足认证性与保密性等安全性质.

关键词：认证与密钥交换协议形式化分析快速登录 ROR模型 Proverif

来源：评论

学校读者我要写书评

暂无评论

基于证据推理和第3代前景理论的不确定性多属性决策方法

引用

控制与决策 2016年第1期31卷 105-113页

作者：靳留乾徐扬西南交通大学四川省系统可信性自动验证工程实验室成都610031 西南交通大学经济管理学院成都610031

针对多状态不确定性多属性决策问题,建立基于证据推理和第3代前景理论的决策方法.首先,给出不确定性知识表示方法—–确定因子结构及其构造方法;然后,将第3代前景理论构造价值函数和确定权重函数引入决策方法中,得到每个方案在各属性下... 详细信息

针对多状态不确定性多属性决策问题,建立基于证据推理和第3代前景理论的决策方法.首先,给出不确定性知识表示方法—–确定因子结构及其构造方法;然后,将第3代前景理论构造价值函数和确定权重函数引入决策方法中,得到每个方案在各属性下的前景价值;进一步,根据证据推理方法对前景价值进行信息融合得到各方案的合成前景价值,并依据合成前景价值对方案进行排序;最后,通过算例验证了所提出方法的可行性和有效性.

关键词：不确定性多属性决策确定因子结构证据推理第3代前景理论参考点

来源：评论

学校读者我要写书评

暂无评论

利用逻辑演绎求解SAT问题的启发式完全算法

引用

西南交通大学学报 2017年第6期52卷 1224-1232页

作者：陈青山徐扬何星星西南交通大学信息科学与技术学院四川成都610031 西南交通大学系统可信性自动验证国家地方联合工程实验室四川成都610031

为解决可满足性(satisfiability problem,SAT)问题求解过程中分支决策效率不高的问题,提出了一种基于逻辑演绎分组(logical deduction group,LDG)的启发式完全算法.该算法通过选择剩余未满足子句参与逻辑演绎,得到一组局部可满足赋值序... 详细信息

为解决可满足性(satisfiability problem,SAT)问题求解过程中分支决策效率不高的问题,提出了一种基于逻辑演绎分组(logical deduction group,LDG)的启发式完全算法.该算法通过选择剩余未满足子句参与逻辑演绎,得到一组局部可满足赋值序列,并引导求解器优先搜索赋值序列所在解空间;对于可满足问题,可以通过迭代调用演绎过程,将局部可满足解成组地扩充为全局可满足解,对于不可满足问题,如果演绎结果出现空子句,则可以直接判定.采用SAT国际竞赛的实例,与具有代表性的指数级变元状态独立下降和(exponential variable state independent decaying sum,EVSIDS)变量决策算法进行了对比测试,结果表明:在求解总问题数方面,LDG比EVSIDS多出42个;在求解速度方面,LDG对可满足问题的求解时间相较EVSIDS平均减少了22.8%,对不可满足问题的求解时间平均减少了17.8%,总平均时间减少了20.1%.

关键词： SAT问题启发式算法搜索算法变量决策演绎推理

来源：评论

学校读者我要写书评

暂无评论

基于形式化方法的道口控制系统规范建模与验证

引用

西南交通大学学报 2019年第3期54卷 573-578,603页

作者：王恪铭王峥西南交通大学信息科学与技术学院四川成都611756 西南交通大学系统可信性自动验证国家地方联合工程实验室四川成都610031

为了增强铁路道口控制系统设计的可靠性,使用一种形式化方法对该系统进行建模与验证.基于道口管理规范,在分析系统各类属性与事件流程的基础上,使用 UML 图方法并结合精化策略建立了系统各层的 Event-B语言模型.通过对不变式的证明义务... 详细信息

为了增强铁路道口控制系统设计的可靠性,使用一种形式化方法对该系统进行建模与验证.基于道口管理规范,在分析系统各类属性与事件流程的基础上,使用 UML 图方法并结合精化策略建立了系统各层的 Event-B语言模型.通过对不变式的证明义务进行证明,验证了系统设计中的安全、时间特性,检查出了需求规范分析中的缺陷,提出了增强系统稳健性的改进方案,修正了系统的设计原型.最后,通过不变式冲突与死锁检验进一步确认了模型的正确性.研究表明文中方法提高了形式化建模过程的准确性与层次性,且确认得出目前规范中存在列车驶入道口时不能确保道口出清的缺陷,证实了使用本文形式化流程可以验证道口控制系统的需求规范并形成可靠的设计原型,从而可提高铁路道口的安全性.

关键词：铁路运输铁路道口需求规范形式化方法系统设计模型验证

来源：评论

学校读者我要写书评

暂无评论

一阶逻辑中的扩展子句消去原则

引用

西南交通大学学报 2020年第3期55卷 588-595页

作者：宁欣然徐扬何星星西南交通大学系统可信性自动验证国家地方联合工程实验室四川成都610031 西南交通大学信息科学与技术学院四川成都610031 西南交通大学数学学院四川成都610031

对于一阶逻辑定理证明器,子句集化简一直是必不可少的步骤,这将有助于提高后续一阶逻辑定理证明器的证明效率.针对子句冗余性的判断,提出了一种评估子句冗余性的原则:集合蕴涵模归结原则.并且证明了该原则在不带等词一阶逻辑上的可靠性... 详细信息

对于一阶逻辑定理证明器,子句集化简一直是必不可少的步骤,这将有助于提高后续一阶逻辑定理证明器的证明效率.针对子句冗余性的判断,提出了一种评估子句冗余性的原则:集合蕴涵模归结原则.并且证明了该原则在不带等词一阶逻辑上的可靠性,根据该原则删除子句,不会影响原始子句集的不可满足性或者可满足性.此外,依据该原则提出了两种新型的一阶逻辑预处理方法:集合归结包含消去(set resolution subsumption,SRSE)方法和集合归结不对称恒真消去(set resolution asymmetric tautology elimination,SRATE)方法,并证明了这两种子句消去方法在不带等词一阶逻辑子句集上的可靠性.最后在理论上比较了SRSE方法和归结包含消去(sesolution subsumption elimination,RSE)方法以及SRATE方法和归结不对称恒真(sesolution asymmetric tautology elimination,RATE)方法之间的有效性,结果表明SRSE方法和SRATE方法分别比RSE方法和RATE方法更为有效.

关键词：集合蕴涵模归结一阶逻辑蕴涵模归结子句消去方法预处理方法

来源：评论

学校读者我要写书评

暂无评论

基于OpenMP的并行遗传算法求解SAT问题

引用

西南交通大学学报 2019年第2期54卷 428-435页

作者：吴贯锋徐扬常文静陈树伟徐鹏西南交通大学信息科学与技术学院四川成都610031 西南交通大学系统可信性自动验证国家地方联合工程实验室四川成都610031 西南交通大学数学学院四川成都610031

为了提高SAT (boolean satisfiability)问题求解效率,在OpenMP (open multi-processing)编程框架下,将遗传算法与局部搜索算法结合,改进了混合遗传算法中的选择算法,将原有选择操作的时间复杂度降低到O(N)级别.算法采用OpenMP中的编译... 详细信息

为了提高SAT (boolean satisfiability)问题求解效率,在OpenMP (open multi-processing)编程框架下,将遗传算法与局部搜索算法结合,改进了混合遗传算法中的选择算法,将原有选择操作的时间复杂度降低到O(N)级别.算法采用OpenMP中的编译制导语句#pragma omp parallel粗粒度并行化驱动混合遗传算法,采用#pragma omp single语句块实现了子种群间个体的同步迁移操作.与同类算法HCGA (hybrid cloud genetic algorithm)比较分析表明:改进算法HGA (hybrid genetic algorithm)以及并行后的混合遗传算法CGPHGA(coarse-grained parallel hybrid genetic algorithm)在求解成功率和求解效率上都有显著提高,部分问题求解成功率提高达5倍.

关键词： SAT问题 OpenMP 并行混合遗传算法粗粒度模型

来源：评论

学校读者我要写书评

暂无评论

多元协同演绎在一阶逻辑ATP中的应用

引用

西南交通大学学报 2020年第2期55卷 401-408,427页

作者：曹锋徐扬陈树伟吴贯锋常文静西南交通大学信息科学与技术学院四川成都610031 西南交通大学系统可信性自动验证国家地方联合工程实验室四川成都610031 西南交通大学数学学院四川成都610031

一阶逻辑是数理逻辑中重要的分支,对其逻辑公式的自动推理是人工智能领域重要的研究热点之一.目前一阶逻辑自动定理证明大多采用二元归结方法,每次只有2个子句进行归结,只消去1组互补对,导致演绎归结式文字数较多,影响了演绎效率.为此,... 详细信息

一阶逻辑是数理逻辑中重要的分支,对其逻辑公式的自动推理是人工智能领域重要的研究热点之一.目前一阶逻辑自动定理证明大多采用二元归结方法,每次只有2个子句进行归结,只消去1组互补对,导致演绎归结式文字数较多,影响了演绎效率.为此,基于矛盾体分离规则提出了一种多元协同演绎算法,该算法每次允许多个子句进行协同演绎,消去多组互补对,从而演绎分离式文字数较少且可控,能有效提高推理能力;并且,该算法通过有效演绎权重和无效演绎权重调整子句演绎顺序,利用回溯机制搜索较优路径,有效规划演绎路径.将该算法应用于国际顶尖证明器Eprover 2.1,以CADE2017竞赛例(FOF组)为测试对象,对加入多元协同演绎算法的Eprover 2.1证明器进行试验.试验结果表明其能力超过了Eprover 2.1:多证明定理8个;能证明Eprover 2.1未证明定理31个,占未证明总数的28.2%.

关键词：数理逻辑人工智能定理证明二元归结矛盾体分离规则

来源：评论

学校读者我要写书评

暂无评论

基于边权重图神经网络的一阶逻辑前提选择

引用

西南交通大学学报 2022年第6期57卷 1368-1375页

作者：刘清华徐扬吴贯锋李瑞杰西南交通大学信息科学与技术学院四川成都611756 西南交通大学系统可信性自动验证国家地方联合工程实验室四川成都610031 西南交通大学数学学院四川成都611756 西南交通大学交通运输与物流学院四川成都611756

为提高自动定理证明器在大规模问题中证明问题的能力,前提选择任务应运而生.由于公式图的有向性,主流的图神经网络框架只能单向地对节点进行更新,且无法编码公式图中子节点间的顺序.针对以上问题,提出了带有边类型的双向公式图表示方法... 详细信息

为提高自动定理证明器在大规模问题中证明问题的能力,前提选择任务应运而生.由于公式图的有向性,主流的图神经网络框架只能单向地对节点进行更新,且无法编码公式图中子节点间的顺序.针对以上问题,提出了带有边类型的双向公式图表示方法,并提出了一种基于边权重的图神经网络(edge-weight-based graph neural network,EW-GNN)模型用于编码一阶逻辑公式.该模型首先利用相连节点的信息来更新对应边类型的特征表示,随后利用更新后的边类型特征计算邻接节点对中心节点的权重,最后利用邻接节点的信息双向地对中心节点进行更新.实验比较分析表明:基于边权重的图神经网络模型在前提选择任务中表现得更加优越,其在相同的测试集上比当前最优模型的分类准确率高了约1%.

关键词：图神经网络双向图前提选择一阶逻辑公式

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：