自动定理证明

作品数：40被引量：39H指数：3
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：孙吉贵刘全李兆鹏陈意云缪淮扣更多>>
相关机构：中国科学技术大学吉林大学上海大学西南交通大学更多>>
相关期刊：《西南交通大学学报》《中关村》《南京建筑工程学院学报》《模式识别与人工智能》更多>>
相关基金：国家自然科学基金国家高技术研究发展计划吉林省自然科学基金高等学校骨干教师资助计划更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
矛盾体分离单元结果演绎方法及应用
《计算机工程与科学》2024年第12期2252-2260,共9页曹锋 谢燏 易见兵 李俊 
国家自然科学基金(62366017,62066018);江西省教育厅项目(GJJ200818,GJJ210828);赣州市科技计划项目(GZKJ20206030);江西理工大学博士启动基金(205200100060)。
一阶逻辑自动定理证明是人工智能领域重要的研究内容。为提高单元结果归结演绎效率,提出了一种新的基于多元、动态、协同的单元结果演绎方法,称为矛盾体分离单元结果演绎方法,并详细地给出了其演绎定义、演绎方法、演绎的优势分析及算...
关键词：一阶逻辑 自动定理证明 人工智能 单元结果归结 矛盾体分离规则 
基于大模型的引理辅助线性数据结构定理自动证明
《江西师范大学学报(自然科学版)》2024年第5期459-463,共5页万亮亮 刘艳娇 龙海建 王昌晶 
国家自然科学基金(62462037);江西省主要学科学术与技术带头人培养课题(20232BCJ22013);江西省教育厅科学技术重点课题(GJJ2200302)资助项目.
该文利用大语言模型(large language models,LLMs)与形式化验证技术实现线性数据结构定理的自动证明,并提出通过引入引理来提高线性数据结构定理证明效率的方法.首先,利用LLMs生成定理的非形式化证明及形式化证明草图;然后,基于非形式...
关键词：大语言模型 提示工程 自动定理证明 Isabelle/HOL 形式化验证 
基于符号权重的一阶逻辑前提选择方法
《西南交通大学学报》2023年第3期704-710,共7页刘清华 李瑞杰 朱绪胜 陈代鑫 
国家自然科学基金(72101217)。
为增强自动定理证明器从一阶逻辑问题的大规模前提中选择相关前提的能力,首先,提出符号权重计算公式,基于符号在问题中出现的频率获取不同符号对应的权重;其次,提出相关度计算公式,利用分配的符号权重计算问题中前提和结论间的相关度;同...
关键词：前提选择 自动定理证明 一阶逻辑 
符号主义人工智能的历史回顾及其哲学审视被引量：4
《武陵学刊》2023年第2期34-41,共8页陈明益 张友恒 
中央高校基本科研业务费专项资金资助“人工智能与伦理道德的深度互动研究”(2021VI011);武汉理工大学教学改革研究项目“新文科理念下‘马克思主义基本原理概论’课程建设研究”(w20210173)。
符号主义作为AI研究的最初范式,其发展经历了自动定理证明、专家系统和知识图谱三个主要阶段,对现代AI的理论及其应用作出了重要贡献。作为AI领域首个探索和构建智能的范式,它涉及诸多哲学问题,这引起了AI专家和哲学家的共同兴趣,他们...
关键词：符号主义 自动定理证明 专家系统 知识表示 人工智能哲学 
人工智能在食品安全方面的应用被引量：1
《中国无机分析化学》2023年第4期I0001-I0001,共1页肖湘萍 
目前,电脑网络通信、人工智能(通俗地说,指的主要是机器人)、大型数据库、多媒体技术一起,构成了信息科技的四大热门领域。人工智能是一门涉及信息学、逻辑学、认知学、思维学、系统学和生物学的多学科交叉技术,已在知识处理、模式识别...
关键词：人工智能 自然语言处理 自动程序设计 智能机器人 自动定理证明 机器学习 多媒体技术 模式识别 
易变数据结构归纳引理的自动证明
《电子技术（上海）》2017年第6期61-66,58,共7页杨晨 罗奇鸣 李薛剑 陈意云 
程序性质的自动验证有时需要验证者提供相关的归纳引理,程序验证的结果可靠与否依赖于验证者所提供的归纳引理正确与否。本文围绕操作易变数据的程序的自动验证,设计并实现一个相关引理的自动证明器,作为程序自动验证器中检查验证者所...
关键词：程序验证 易变数据结构 结构归纳 自动定理证明 
形状图理论的定理证明被引量：4
《计算机学报》2016年第12期2460-2480,共21页张昱 陈意云 李兆鹏 
国家“八六三”高技术研究发展计划项目基金(2012AA010901);国家自然科学基金(61170018,61229201)资助~~
验证操作易变数据结构的指针程序仍面临很多挑战.数据结构中严重的指针别名显著地复杂化对操作这些结构的程序的推理.为分析和验证操作易变数据结构的指针程序,文中提出了形状图逻辑.形状图是描述程序中静态声明的堆指针变量和动态分配...
关键词：形状图逻辑 形状分析 程序验证 自动定理证明 循环不变式的推断 
人工智能:光荣与梦想
《中关村》2016年第6期74-75,共2页刘卓军 
＂狗＂之光荣的背后是技术、是实力,是人的智慧。现年97岁的数学家吴文俊教授依旧精神矍铄,他曾经明确指出：机器的出现延伸了人的体力,而现代计算机的出现则延伸了人的脑力。受技术进步的影响,吴先生在近花甲之年,以他深厚的数学功底...
关键词：数学机械化 自动定理证明 刻苦精神 机器智能 吴方法 技术进步 吴文俊 数学界 人类智能 计算机科学 
程序验证中归纳性质定理的自动证明
《电子技术（上海）》2015年第8期1-6,共6页郝爔 
国家自然科学基金(61170018;61229201)资助
基于演绎推理的程序验证系统原型的功能往往受限于断言语言的表达能力、循环不变式的自动推断能力和自动定理证明器的证明能力。文章为了增强程序断言语言对程序性质的表达能力,为系统原型引入了自定义归纳谓词。此外,为了减轻自动定理...
关键词：程序验证 归纳定理 自动定理证明 结构归纳 
支持用户自定义谓词的自动定理证明的研究
《小型微型计算机系统》2013年第8期1781-1786,共6页汪娟 李兆鹏 陈意云 
国家自然科学基金项目(61003043;61170018)资助
在先前设计的一个出具证明编译器原型基础上,增加了可用来描述数据结构性质的自定义谓词,对断言语言表达能力方面做了提升.在出具证明编译器的框架内,借助自动定理证明技术,针对自定义谓词的特点,设计了专门的推理规则,由此实现自定义...
关键词：出具证明编译器 自定义谓词 自动定理证明 推理规则 
全选清除导出
共4页<1234>
检索报告 对象比较 聚类工具 使用帮助 返回顶部