检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

一阶逻辑定理证明器中的无效子句删除策略

计算机应用 2024年第3期44卷 677-682页

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

在一阶逻辑定理证明器中,子句预处理是不可或缺的步骤,而子句的消去规则是预处理中极其重要的部分。传统的基于纯文字规则的子句消去方法在理论上存在子句删除过多的问题,在算法实现上又存在子句删除不充分的情况。为了提高子句删除的... 详细信息

在一阶逻辑定理证明器中,子句预处理是不可或缺的步骤,而子句的消去规则是预处理中极其重要的部分。传统的基于纯文字规则的子句消去方法在理论上存在子句删除过多的问题,在算法实现上又存在子句删除不充分的情况。为了提高子句删除的精确率,在理论上,基于纯文字规则对子句进行再分类。第一类称为无效子句,该类子句不能通过等词替换与某个子句形成互补对,此类子句应完全删除;第二类为相对无效子句,该类子句无法与当前子句集中的子句形成互补对,但能进行等词替换,此类子句应在参与演绎后综合考虑是否删除。在算法实现中,考虑到子句的消去应是动态的过程,当前消去的子句会影响已判断的子句的无效性,提出一种用于判定子句无效性的递归遍历算法。将上述子句约简规则应用于证明器CSE1.5(Contradiction Separation Extension 1.5)中,以2019—2022的CADE(Conference on Automated DEduction)自动定理证明(ATP)系统竞赛中一阶逻辑问题组为测试对象。在300 s内,应用所提算法的CSE1.5_IC比原始CSE1.5总共多证明了27个问题。在两个版本证明器共同证明的所有FNE(FOF theorems without Equality)测试例中,CSE1.5_IC比CSE1.5平均每个问题多约简了28个子句,平均求解时间减少了7.07 s。实验结果表明,所提无效子句约简算法是一种有效的预处理方式,能够提高一阶逻辑子句集的约简精确率,同时能够提高自动定理证明器的证明能力和缩短证明时间。

关键词：自动推理一阶逻辑子句删除纯文字规则无效子句

自动推理技术在求解组合数学难题中的研究进展

在线全文

学校读者我要写书评

暂无评论

计算机科学 2023年第7期50卷 167-175页

作者：黄沛刘明昊马菲菲张健中国科学院软件研究所计算机科学国家重点实验室北京100190 中国科学院软件研究所并行软件与计算科学实验室北京100190 中国科学院大学北京100049

自动推理是一种以符号演算的方式来自动模拟人类逻辑推理能力的技术,其总体目标是利用计算机构建一个将不同形式的推理机械化的系统。虽然该领域的理论框架尚未实现对人类全部推理能力的模拟,但该领域的发展已经可以帮助研究人员解决一... 详细信息

自动推理是一种以符号演算的方式来自动模拟人类逻辑推理能力的技术,其总体目标是利用计算机构建一个将不同形式的推理机械化的系统。虽然该领域的理论框架尚未实现对人类全部推理能力的模拟,但该领域的发展已经可以帮助研究人员解决一些数学和逻辑领域的开放性问题,并提供了计算科学中的重要应用。文中简要回顾了利用自动推理技术处理组合数学开放性难题时的代表性方法,重点梳理了该领域的国内外最新进展,分析了各种方法的优势与不足,介绍了近年来出现的增强自动推理结果可信性的技术方法,并探讨了未来的研究方向和面临的挑战。

关键词：自动推理组合数学计算逻辑人工智能符号演算

在线全文

学校读者我要写书评

暂无评论

法国军事人工智能力量几何?

兵器知识 2024年第3期 64-68页

作者：一延不详

法国在人工智能的基础数学理论领域有着丰富的学术底蕴。历史上,法国是诸多数学思想的发源地,笛卡尔、费马等著名数学家都是法国人。“数学界的诺贝尔奖”菲尔兹奖得主有接近五分之一是法国人。表彰运用计算机等工具实现自动定理证明的... 详细信息

法国在人工智能的基础数学理论领域有着丰富的学术底蕴。历史上,法国是诸多数学思想的发源地,笛卡尔、费马等著名数学家都是法国人。“数学界的诺贝尔奖”菲尔兹奖得主有接近五分之一是法国人。表彰运用计算机等工具实现自动定理证明的大奖被命名为“埃尔布朗自动推理杰出成就奖”,而埃尔布朗正是法国数学家。自动定理证明可以被看作人工智能的先驱。1994年获得埃尔布朗奖的布莱塞就曾担任美国人工智能学会主席。丰富的数学人才给法国发展人工智能提供了有利条件,机器学习先驱杨立坤也是法国人。荣获菲尔兹奖的法国数学家塞德里克·维拉尼的发现为深度学习算法优化奠定了重要理论基础。法国在人工智能的重要领域神经形态计算上也独树一帜,卓有建树。

关键词：人工智能杰出成就奖机器学习法国数学家自动推理德里克著名数学家学术底蕴

基于知识库与案例库的在线健康社区诊疗解决方案自动推理模型研究

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

情报科学 2022年第5期40卷 161-172页

作者：盛姝黄奇郭进京解绮雯杨洋南京大学信息管理学院江苏南京210046 南京大学国家信息资源管理南京研究基地江苏南京210093

【目的/意义】作为医疗与管理科学领域最为重要的研究课题之一,在线健康社区智能诊疗在我国“互联网+医疗”新业态发展背景下扮演重要角色。【方法/过程】本文从本体论与CBR视角出发,构建基于知识库与案例库的在线健康社区诊疗解决方案... 详细信息

【目的/意义】作为医疗与管理科学领域最为重要的研究课题之一,在线健康社区智能诊疗在我国“互联网+医疗”新业态发展背景下扮演重要角色。【方法/过程】本文从本体论与CBR视角出发,构建基于知识库与案例库的在线健康社区诊疗解决方案自动推理模型;通过八爪鱼采集器获取“好大夫在线”疾病科普以及医患问答数据构建本体,并利用文本分析挖掘出可解释的疾病知识及解决方案,分别实现知识库与案例库的半自动构建;以成年人先天性心脏病为例,将ACHD-AP进行形式化定义,采用推理引擎对患者案例进行风险分类及划分至对应的疾病知识库,并实现诊疗解决方案的自动推理。【结果/结论】研究显示,本文诊疗解决方案推理结论与专家建议相似度较高,且OntoQA评估下的知识库以及案例库本体层次结构关系合理。【创新/局限】基于知识库与案例库的诊疗解决方案自动推理模型为后续在线健康社区实现智能诊疗以及服务模式的创新提供了方法上的参考。

关键词：在线健康社区知识库案例库诊疗解决方案自动推理

在线全文

学校读者我要写书评

暂无评论

一种基于集合符号的自动推理扩展方法

计算机研究与发展 2007年第8期44卷 1317-1323页

作者：刘全伏玉琛孙吉贵崔志明龚声蓉凌兴宏苏州大学计算机科学与技术学院吉林大学符号计算与知识工程教育部重点实验室长春130012

在多值逻辑Tableau推理的基础上,提出了一种基于集合符号的自动推理扩展方法.将符号集合作为真值,减少了Tableau的推理分枝,并可以将适合经典逻辑的推理方法和策略应用于其中,使得非经典逻辑推理经典化.使用SWI-PROLOG语言设计实现了基... 详细信息

在多值逻辑Tableau推理的基础上,提出了一种基于集合符号的自动推理扩展方法.将符号集合作为真值,减少了Tableau的推理分枝,并可以将适合经典逻辑的推理方法和策略应用于其中,使得非经典逻辑推理经典化.使用SWI-PROLOG语言设计实现了基于集合符号的自动推理系统,在系统中使用集合符号方法,只需要在规则库中增加推理规则,即可生成规则程序,系统本身不需要任何的修改,因此一些适合于经典逻辑的推理方法和技巧就可以很容易地应用到多值逻辑、模态逻辑、直觉逻辑等非经典逻辑,也可以进一步推广到无穷值逻辑和含模糊量词(如T-算子和S-算子)的逻辑中,对于无穷值逻辑和模糊逻辑的Tableau方法研究具有一定的借鉴作用.对TPTP中的900个逻辑问题进行了证明,实验结果表明,系统在时间和空间上效率都是较高的.

关键词：集合符号自动推理 Tableau 经典逻辑非经典逻辑

在线全文

学校读者我要写书评

暂无评论

基于路径搜索的格值命题逻辑自动推理方法

西南交通大学学报 2003年第3期38卷 248-252页

作者：李海明刘鹏仙徐扬西南交通大学应用数学系四川成都640031 唐山师范学院计算机系河北唐山063000

提出一种基于路径搜索的自动推理算法.除了采取预处理外,还采用了动态的删除策略,使对大部分路径的搜索变成对一条路径搜索.可快速地完成对一类格值命题逻辑中的任何一个子句集可满足性与不可满足性的判定.文中还讨论了该算法计算的复杂性.

关键词：自动推理路径搜索格值命题逻辑删除策略子句集互补对计算复杂性

在线全文

学校读者我要写书评

暂无评论

基于自动推理技术的智能规划方法

软件学报 2009年第5期20卷 1226-1240页

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

对几种智能规划方法中利用的逻辑演绎与推理技术予以分析,分别介绍利用命题逻辑的基于可满足性的规划方法与规划系统,利用模态逻辑与析取推理的Conformant规划方法与规划系统,利用非单调逻辑的规划方法和利用模糊描述逻辑的Flexible规... 详细信息

对几种智能规划方法中利用的逻辑演绎与推理技术予以分析,分别介绍利用命题逻辑的基于可满足性的规划方法与规划系统,利用模态逻辑与析取推理的Conformant规划方法与规划系统,利用非单调逻辑的规划方法和利用模糊描述逻辑的Flexible规划方法,并结合国际规划竞赛和相关论文等的实验结论说明上述方法的有效性和可行性.最后,提出目前基于自动推理技术的智能规划方法所面临的挑战、可能的处理方法以及与之相关的研究热点与趋势.

关键词：智能规划命题逻辑模态逻辑非单调逻辑描述逻辑自动推理可满足性

Fuzzy关系模式映射反演与犯罪侦查自动推理

在线全文

学校读者我要写书评

暂无评论

模式识别与人工智能 2003年第1期16卷 70-75页

作者：何平辽宁警官高等专科学校大连116033

本文首次将Fuzzy关系模式映射反演原则(FRPMI)应用于犯罪侦查自动推理中,提出了Fuzzy定映自动推理框架。通过实际犯罪模式与现场表现模式的关系结构,建立了两种模式映射。研究表明,在计算机中建立案件现场与破案线索的规范集是自动推理... 详细信息

本文首次将Fuzzy关系模式映射反演原则(FRPMI)应用于犯罪侦查自动推理中,提出了Fuzzy定映自动推理框架。通过实际犯罪模式与现场表现模式的关系结构,建立了两种模式映射。研究表明,在计算机中建立案件现场与破案线索的规范集是自动推理的前提,而补充线索是关键。作者认为,自动推理的可靠性决定于人机交互作用,同时破案线索的选择要通过综合评价来决定,并且不能缺少自学习和直觉与理性的判断。

关键词：映射反演犯罪侦查自动推理人工智能专家系统不确性推理模糊关系模式

基于结构分析的局部Gibbs抽样自动推理算法

在线全文

学校读者我要写书评

暂无评论

模式识别与人工智能 2013年第4期26卷 382-391页

作者：王浩曹龙雨姚宏亮李俊照合肥工业大学计算机与信息学院合肥230009

提出一种基于结构分析的局部Gibbs抽样的贝叶斯网络推理算法(S-LGSI).S-LGSI算法基于联合树算法的概率图模型分析思想,对贝叶斯网络进行精确分解,然后根据查询结点和证据结点生成具有强相关性的局部网络模型,进而对局部网络模型进行Gibb... 详细信息

提出一种基于结构分析的局部Gibbs抽样的贝叶斯网络推理算法(S-LGSI).S-LGSI算法基于联合树算法的概率图模型分析思想,对贝叶斯网络进行精确分解,然后根据查询结点和证据结点生成具有强相关性的局部网络模型,进而对局部网络模型进行Gibbs抽样推理.与当前基于抽样的其它近似推理算法相比,该算法降低推理的计算维数.同时,由于局部抽样模型包含了与查询结点相关的重要信息,因此该算法保证局部抽样推理的精度.算法分析和在Alarm网的实验结果表明,S-LGSI算法较显著降低时间复杂度,同时也提高推理精度.S-LGSI算法应用于上海证券交易所股票网络的推理结果与实际情况基本一致,表现出较强的实用性.

关键词：自动推理贝叶斯网络马尔科夫蒙特卡洛吉布斯抽样