一阶逻辑

作品数：189被引量：315H指数：7
导出分析报告
相关领域：自动化与计算机技术哲学宗教更多>>
相关作者：徐扬陈树伟何星星孙吉贵刘新文更多>>
相关机构：西南交通大学中国社会科学院哲学研究所吉林大学北京大学更多>>
相关期刊：更多>>
相关基金：国家自然科学基金国家高技术研究发展计划中央高校基本科研业务费专项资金国家社会科学基金更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
一阶逻辑定理证明器CSE中矛盾体分离式的简化方法
《计算机科学》2025年第5期235-240,共6页吴鑫 陈树伟 姜世攀 
国家自然科学基金(61976130)。
一阶逻辑自动定理证明器能够解决大量形式化后的实际问题,具有重要的应用价值。矛盾体分离演绎发展了自动定理证明领域经典的归结原理,具有更强的证明能力。在基于矛盾体分离规则的自动定理证明器CSE(Contradiction Separation Extensi...
关键词：矛盾体分离 矛盾体分离式简化 最简矛盾体分离式 互补信息 证明器 
一阶逻辑中逻辑度量空间与理论相容性的拓扑性质
《湖北大学学报(自然科学版)》2025年第2期173-179,共7页王前 惠小静 袁一丹 许倩 
国家自然科学基金(12261090、12301456);延安大学研究生教育创新计划项目;延安大学创新训练项目(YCX2023011)资助。
设Φ是全体不含函数符号的一阶闭逻辑公式之集。本研究基于一阶逻辑中的公理化真度理论对逻辑度量空间的结构进行分析,搭建逻辑度量空间与拓扑概念之间的联系,证明逻辑度量空间(Φ,ρ)中没有孤立点,并且度量空间(Φ,ρ)存在着既开又闭...
关键词：一阶逻辑 逻辑度量空间 零维空间 相容性 
基于多属性决策的一阶逻辑子句选择方法
《西南交通大学学报》2025年第1期185-193,共9页曾国艳 徐扬 陈树伟 姜世攀 
国家自然科学基金项目(61976130)。
基于一阶逻辑的自动定理证明器(ATP)在知识表达和自动推理研究中占据重要地位,而启发式策略则是提升ATP性能的关键研究方向.主流的启发式策略通常通过描述子句属性来确定属性优先级,从而选择子句,但属性优先级受人为因素影响,且评估子...
关键词：一阶逻辑 矛盾体分离规则 启发式策略 多属性决策 熵权法 
一种基于子句稳定度的多元动态演绎算法及应用
《广西师范大学学报（自然科学版）》2024年第6期164-176,共13页曹锋 王家帆 易见兵 李俊 
国家自然科学基金(62366017,62066018);江西省教育厅项目(GJJ200818,GJJ210828);赣州市科技计划项目(GZKJ20206030);江西理工大学博士启动基金(205200100060)。
一阶逻辑自动定理证明是人工智能领域的核心基础。启发式策略在提升一阶逻辑自动定理证明器方面备受关注,其中根据子句属性选择较优子句参与演绎为重要的研究内容。基于矛盾体分离规则,将子句中的文字分为构建标准矛盾体的文字和构建矛...
关键词：一阶逻辑 定理证明 人工智能 启发式策略 多元动态演绎 
策略动态组合优化多元演绎算法及应用
《浙江大学学报（理学版）》2024年第6期732-739,共8页郭海林 曹锋 易见兵 李俊 吴贯锋 
国家自然科学基金资助项目(62366017,62066018,62106206);江西省科技厅项目(20212ACB202003);江西省教育厅项目(GJJ200818,GJJ180482);江西理工大学博士启动基金(205200100060).
一阶逻辑自动定理证明是人工智能领域重要的研究分支,其中子句选择策略对于提升定理证明能力具有重要作用。多元矛盾体分离演绎具有许多良好的演绎特性。为更好地指导多元演绎中的子句选择,提出了一种策略动态组合优化多元演绎方法,通...
关键词：一阶逻辑 定理证明 人工智能 多元演绎 组合优化 
矛盾体分离单元结果演绎方法及应用
《计算机工程与科学》2024年第12期2252-2260,共9页曹锋 谢燏 易见兵 李俊 
国家自然科学基金(62366017,62066018);江西省教育厅项目(GJJ200818,GJJ210828);赣州市科技计划项目(GZKJ20206030);江西理工大学博士启动基金(205200100060)。
一阶逻辑自动定理证明是人工智能领域重要的研究内容。为提高单元结果归结演绎效率,提出了一种新的基于多元、动态、协同的单元结果演绎方法,称为矛盾体分离单元结果演绎方法,并详细地给出了其演绎定义、演绎方法、演绎的优势分析及算...
关键词：一阶逻辑 自动定理证明 人工智能 单元结果归结 矛盾体分离规则 
子句充分性评估的多元动态演绎算法及应用被引量：1
《华中科技大学学报（自然科学版）》2024年第11期153-160,共8页曹锋 潘世成 易见兵 李俊 
国家自然科学基金资助项目(62066018,62106206)。
为了充分体现子句参与多元动态演绎的灵活性、协同性和充分性,将参与多元演绎的子句划分为主动子句和被动子句,提出一种不同类型的子句充分性评估方法,能较好体现子句的充分性演绎且避免重复路径的搜索.基于该子句评估方法提出一种充分...
关键词：多元动态演绎 回溯机制 演绎路径 一阶逻辑 自动定理证明器 
再论“Being”问题:一种对弗雷格—罗素区分理论的修正方案
《外国哲学》2024年第1期225-244,共20页余欢 
弗雷格—罗素区分理论是在现代一阶逻辑中对“being”含义所作的一种区分性解释,它与传统逻辑以及哲学中对“being”概念更倾向的统合性解释构成了对比。一般这一组对比所反映出来的是传统与现代,以及自然语言与形式符号之间对待“bein...
关键词：BEING 谓述 存在 量化 一阶逻辑 
可满足性模理论综述
《计算机工程与科学》2024年第3期400-415,共16页唐傲 王晓峰 何飞 
国家自然科学基金(62062001);宁夏青年拔尖人才项目(2021)。
可满足性模理论(SMT)是指判定一阶逻辑公式在特定背景理论下的可满足性问题。基于一阶逻辑的SMT相比SAT描述能力更强、抽象能力更高,能处理更加复杂的问题。SMT求解器在各个领域都有应用,已经成为重要的形式化验证引擎。目前,SMT已被广...
关键词：一阶逻辑 可满足性模理论 Lazy方法 DPLL(T) SMT求解器 #SMT 
一阶逻辑定理证明器中的无效子句删除策略被引量：2
《计算机应用》2024年第3期677-682,共6页姜世攀 陈树伟 曾国艳 
国家自然科学基金资助项目(61976130)。
在一阶逻辑定理证明器中,子句预处理是不可或缺的步骤,而子句的消去规则是预处理中极其重要的部分。传统的基于纯文字规则的子句消去方法在理论上存在子句删除过多的问题,在算法实现上又存在子句删除不充分的情况。为了提高子句删除的...
关键词：自动推理 一阶逻辑 子句删除 纯文字规则 无效子句 
全选清除导出
共19页<12345678910>
检索报告 对象比较 聚类工具 使用帮助 返回顶部