定理证明

作品数：1006被引量：857H指数：10
导出分析报告
相关领域：理学自动化与计算机技术更多>>
相关作者：关永施智平李晓娟张杰王国辉更多>>
相关机构：首都师范大学南京航空航天大学北京化工大学华东师范大学更多>>
相关期刊：更多>>
相关基金：国家自然科学基金国际科技合作与交流专项项目国家重点基础研究发展计划国家高技术研究发展计划更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于规则推演提升符号计算的研究
《科学与信息化》2025年第3期80-82,共3页范宇恒 
本文提出一种交互式符号计算方法,旨在提升符号计算的可靠性与深度。该方法通过逐步揭示中间计算结果,能够提高计算过程的透明度,帮助识别潜在的错误并优化计算策略。通过案例研究,实验结果表明该方法在处理较为复杂的数学计算时表现优...
关键词：符号计算 交互式定理证明 基于规则推演 
生物序列比对动态规划算法的统一形式化构造与Isabelle验证
《计算机研究与发展》2025年第1期119-131,共13页石海鹤 蓝孙文 刘日明 石海鹏 王岚 钟林辉 
国家自然科学基金项目(62062039)。
序列比对是生物序列分析中的一个经典问题,旨在找出序列之间的相似性,它对于发现生物序列中的功能、结构和进化信息都具有重要的意义.该问题可分为双序列比对和多序列比对2类,现有工作多针对特定算法展开,没有设计通用的求解方法;此外,...
关键词：序列比对 PAR方法 形式构造 Isabelle定理证明器 
一种基于子句稳定度的多元动态演绎算法及应用
《广西师范大学学报（自然科学版）》2024年第6期164-176,共13页曹锋 王家帆 易见兵 李俊 
国家自然科学基金(62366017,62066018);江西省教育厅项目(GJJ200818,GJJ210828);赣州市科技计划项目(GZKJ20206030);江西理工大学博士启动基金(205200100060)。
一阶逻辑自动定理证明是人工智能领域的核心基础。启发式策略在提升一阶逻辑自动定理证明器方面备受关注,其中根据子句属性选择较优子句参与演绎为重要的研究内容。基于矛盾体分离规则,将子句中的文字分为构建标准矛盾体的文字和构建矛...
关键词：一阶逻辑 定理证明 人工智能 启发式策略 多元动态演绎 
马库恩 用机器证明数学猜想
《环球人物》2024年第24期96-97,共2页尼克 
机器定理证明是人工智能中最古老也最困难的研究领域。在这一领域,威廉·马库恩(1953-2011)可以称得上是最杰出的实干家,他创立的一阶定理证明器Otter是上世纪90年代基于逻辑的定理证明器的集大成者,影响了当时整个定理证明领域的理论...
关键词：定理证明器 数学猜想 人工智能 机器证明 实验室 库恩 实干家 
策略动态组合优化多元演绎算法及应用
《浙江大学学报（理学版）》2024年第6期732-739,共8页郭海林 曹锋 易见兵 李俊 吴贯锋 
国家自然科学基金资助项目(62366017,62066018,62106206);江西省科技厅项目(20212ACB202003);江西省教育厅项目(GJJ200818,GJJ180482);江西理工大学博士启动基金(205200100060).
一阶逻辑自动定理证明是人工智能领域重要的研究分支,其中子句选择策略对于提升定理证明能力具有重要作用。多元矛盾体分离演绎具有许多良好的演绎特性。为更好地指导多元演绎中的子句选择,提出了一种策略动态组合优化多元演绎方法,通...
关键词：一阶逻辑 定理证明 人工智能 多元演绎 组合优化 
矛盾体分离单元结果演绎方法及应用
《计算机工程与科学》2024年第12期2252-2260,共9页曹锋 谢燏 易见兵 李俊 
国家自然科学基金(62366017,62066018);江西省教育厅项目(GJJ200818,GJJ210828);赣州市科技计划项目(GZKJ20206030);江西理工大学博士启动基金(205200100060)。
一阶逻辑自动定理证明是人工智能领域重要的研究内容。为提高单元结果归结演绎效率,提出了一种新的基于多元、动态、协同的单元结果演绎方法,称为矛盾体分离单元结果演绎方法,并详细地给出了其演绎定义、演绎方法、演绎的优势分析及算...
关键词：一阶逻辑 自动定理证明 人工智能 单元结果归结 矛盾体分离规则 
LLRB算法的函数式建模及其机械化验证
《软件学报》2024年第11期5016-5039,共24页左正康 黄志鹏 黄箐 孙欢 曾志城 胡颖 王昌晶 
国家自然科学基金(61862033,62262031);江西省自然科学基金(20212BAB202018);江西省教育厅科技重点项目(GJJ210307)。
基于机器定理证明的形式化验证技术不受状态空间限制,是保证软件正确性、避免因潜在软件缺陷带来严重损失的重要方法.LLRB(left-leaning red-black trees)是一种二叉搜索树变体,其结构比传统的红黑树添加了额外的左倾约束条件,在验证时...
关键词：LLRB 函数式建模 机械化验证 Isabelle定理证明器 二叉搜索树 
基于大模型的引理辅助线性数据结构定理自动证明
《江西师范大学学报(自然科学版)》2024年第5期459-463,共5页万亮亮 刘艳娇 龙海建 王昌晶 
国家自然科学基金(62462037);江西省主要学科学术与技术带头人培养课题(20232BCJ22013);江西省教育厅科学技术重点课题(GJJ2200302)资助项目.
该文利用大语言模型(large language models,LLMs)与形式化验证技术实现线性数据结构定理的自动证明,并提出通过引入引理来提高线性数据结构定理证明效率的方法.首先,利用LLMs生成定理的非形式化证明及形式化证明草图;然后,基于非形式...
关键词：大语言模型 提示工程 自动定理证明 Isabelle/HOL 形式化验证 
图广度优先遍历算法的形式化推导与机械验证方法
《江西师范大学学报(自然科学版)》2024年第5期472-478,共7页余楚凌 曹中雄 王唱唱 王昌晶 
江西省教育厅科学技术研究重点课题(GJJ220302,GJJ210307,GJJ2200303,GJJ220304)资助项目.
针对图广度优先遍历问题,该文提出了一种形式化推导与机械验证方法.首先,描述求解问题的形式化规约,使用分划递推得到统一的循环不变式并开发相应的Apla抽象程序;然后,在Isabelle中描述算法相关的数据类型、定义与基本函数,根据算法程...
关键词：图广度优先遍历 形式化推导 定理证明 循环不变式 
矛盾体分离超演绎方法及应用
《计算机应用》2024年第10期3074-3080,共7页曹锋 杨小玲 易见兵 李俊 
国家自然科学基金资助项目(62366017,62066018);江西省教育厅科研项目(GJJ200818,GJJ210828);赣州市科技计划项目(GZKJ20206030);江西理工大学博士启动基金资助项目(205200100060)。
作为当前自动定理证明器中常用的推理机制,传统基于二元演绎超归结方法的推理过程限定每次有且只有2个子句参与演绎,这种分离的演绎步骤导致演绎缺失导向性和预判性,演绎效率有待提升。为了提升演绎效率,在理论上,针对传统的超归结方法...
关键词：定理证明器 二元演绎 超归结 多元演绎 矛盾体分离 
全选清除导出
共101页<12345678910>
检索报告 对象比较 聚类工具 使用帮助 返回顶部