定理证明器

作品数：35被引量：58H指数：4
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：关永张倩颖施智平王国辉李晓娟更多>>
相关机构：南京航空航天大学首都师范大学江西师范大学清华大学更多>>
相关期刊：《电脑编程技巧与维护》《计算机应用与软件》《南京航空航天大学学报（自然科学版）》《小型微型计算机系统》更多>>
相关基金：国家自然科学基金国家高技术研究发展计划北京市自然科学基金国际科技合作与交流专项项目更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
一阶逻辑定理证明器CSE中矛盾体分离式的简化方法
《计算机科学》2025年第5期235-240,共6页吴鑫 陈树伟 姜世攀 
国家自然科学基金(61976130)。
一阶逻辑自动定理证明器能够解决大量形式化后的实际问题,具有重要的应用价值。矛盾体分离演绎发展了自动定理证明领域经典的归结原理,具有更强的证明能力。在基于矛盾体分离规则的自动定理证明器CSE(Contradiction Separation Extensi...
关键词：矛盾体分离 矛盾体分离式简化 最简矛盾体分离式 互补信息 证明器 
生物序列比对动态规划算法的统一形式化构造与Isabelle验证
《计算机研究与发展》2025年第1期119-131,共13页石海鹤 蓝孙文 刘日明 石海鹏 王岚 钟林辉 
国家自然科学基金项目(62062039)。
序列比对是生物序列分析中的一个经典问题,旨在找出序列之间的相似性,它对于发现生物序列中的功能、结构和进化信息都具有重要的意义.该问题可分为双序列比对和多序列比对2类,现有工作多针对特定算法展开,没有设计通用的求解方法;此外,...
关键词：序列比对 PAR方法 形式构造 Isabelle定理证明器 
马库恩 用机器证明数学猜想
《环球人物》2024年第24期96-97,共2页尼克 
机器定理证明是人工智能中最古老也最困难的研究领域。在这一领域,威廉·马库恩(1953-2011)可以称得上是最杰出的实干家,他创立的一阶定理证明器Otter是上世纪90年代基于逻辑的定理证明器的集大成者,影响了当时整个定理证明领域的理论...
关键词：定理证明器 数学猜想 人工智能 机器证明 实验室 库恩 实干家 
LLRB算法的函数式建模及其机械化验证
《软件学报》2024年第11期5016-5039,共24页左正康 黄志鹏 黄箐 孙欢 曾志城 胡颖 王昌晶 
国家自然科学基金(61862033,62262031);江西省自然科学基金(20212BAB202018);江西省教育厅科技重点项目(GJJ210307)。
基于机器定理证明的形式化验证技术不受状态空间限制,是保证软件正确性、避免因潜在软件缺陷带来严重损失的重要方法.LLRB(left-leaning red-black trees)是一种二叉搜索树变体,其结构比传统的红黑树添加了额外的左倾约束条件,在验证时...
关键词：LLRB 函数式建模 机械化验证 Isabelle定理证明器 二叉搜索树 
矛盾体分离超演绎方法及应用
《计算机应用》2024年第10期3074-3080,共7页曹锋 杨小玲 易见兵 李俊 
国家自然科学基金资助项目(62366017,62066018);江西省教育厅科研项目(GJJ200818,GJJ210828);赣州市科技计划项目(GZKJ20206030);江西理工大学博士启动基金资助项目(205200100060)。
作为当前自动定理证明器中常用的推理机制,传统基于二元演绎超归结方法的推理过程限定每次有且只有2个子句参与演绎,这种分离的演绎步骤导致演绎缺失导向性和预判性,演绎效率有待提升。为了提升演绎效率,在理论上,针对传统的超归结方法...
关键词：定理证明器 二元演绎 超归结 多元演绎 矛盾体分离 
基于定理证明器的行波进位加法器开发以及新的芯片设计方法探索
《微电子学与计算机》2024年第10期95-105,共11页孟月华 陈乡栎 陈钢 
数字芯片的规模已经进入几百亿晶体管的时代,传统的硬件设计方法难以应对日益复杂的电路需求,比如基于Verilog语言的硬件设计。针对这个问题,文章以行波进位加法器为例,探索基于交互式定理证明器Coq的芯片设计方法,该方法不仅在Coq中完...
关键词：定理证明器 芯片设计 COQ 行波进位加法器 
基于二幂阶矩阵的量子中间表示与翻译
《计算机应用》2024年第10期3141-3150,共10页陶文萱 陈钢 
在两能级量子计算系统中,所有量子门、量子态和测量算子都可以表示为2的幂次方阶矩阵(简称二幂阶矩阵)的形式,而现有量子编程语言未考虑该特性。因此,提出一种二幂阶矩阵类型系统,并设计相应的量子中间表示。首先,在定理证明器Coq中利...
关键词：量子计算 类型系统 量子中间表示 定理证明器 COQ 
微内核操作系统互斥量模块功能正确性的形式化验证
《软件学报》2024年第9期4179-4192,共14页张林雁 李希萌 施智平 关永 曹钦翔 张倩颖 
国家自然科学基金(62002246,62272322,62272323,62372311,62372312,61902240)。
操作系统在许多安全攸关领域为软件系统提供关键性底层支撑,操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障,造成巨大经济损失或危及人身安全.为了减少此类安全事故的发生,对操作系统正确性进行验证十分必要.传统测...
关键词：互斥量 功能正确性 形式化验证 定理证明 Coq定理证明器 
一阶逻辑定理证明器中的无效子句删除策略被引量：2
《计算机应用》2024年第3期677-682,共6页姜世攀 陈树伟 曾国艳 
国家自然科学基金资助项目(61976130)。
在一阶逻辑定理证明器中,子句预处理是不可或缺的步骤,而子句的消去规则是预处理中极其重要的部分。传统的基于纯文字规则的子句消去方法在理论上存在子句删除过多的问题,在算法实现上又存在子句删除不充分的情况。为了提高子句删除的...
关键词：自动推理 一阶逻辑 子句删除 纯文字规则 无效子句 
基于函数式语义的循环和递归程序结构通用证明技术
《软件学报》2023年第8期3686-3707,共22页李希萌 王国辉 张倩颖 施智平 关永 
国家重点研发计划(2019YFB1309900);国家自然科学基金(61876111,61877040,62002246);北京市教育委员会科技计划(KM201910028005,KM202010028010)。
各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明...
关键词：程序验证 大步操作语义 定理证明 Coq定理证明器 
全选清除导出
共4页<1234>
检索报告 对象比较 聚类工具 使用帮助 返回顶部