检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

支持索引式的PPTL定理证明器的实现

软件学报 2022年第6期33卷 2172-2188页

作者：王小兵寇蒙莎李春奕赵亮西安电子科技大学计算机科学与技术学院陕西西安710071

定理证明是目前主流的形式化验证方法,拥有强大的抽象和逻辑表达能力,且不存在状态空间爆炸问题,可用于有穷和无穷状态系统,但其不能完全自动化,并且要求用户掌握较强的数学知识.含索引式的命题投影时序逻辑(PPTL)是一种具有完全正则表... 详细信息

定理证明是目前主流的形式化验证方法,拥有强大的抽象和逻辑表达能力,且不存在状态空间爆炸问题,可用于有穷和无穷状态系统,但其不能完全自动化,并且要求用户掌握较强的数学知识.含索引式的命题投影时序逻辑(PPTL)是一种具有完全正则表达能力,并且包含LTL的时序逻辑,具有较强的建模和性质描述能力.目前,一个可靠完备的含索引式的PPTL公理系统已被构建,然而基于该公理系统的定理证明尚未得到良好工具的支持,存在证明自动化程度较低以及证明冗长易错的问题.鉴于此,首先设计了支持索引式的PPTL定理证明器的实现框架,包括公理系统的形式化与交互式定理证明;然后,在Coq中形式化定义了含索引式的PPTL公式、公理与推理规则,完成了框架中公理系统的实现;最后,通过两个实例的交互式证明验证了该定理证明器的可用性.

关键词：定理证明 Coq 索引式命题投影时序逻辑公理系统

以太坊智能合约定理证明中的形式化规约研究综述

在线全文

学校读者我要写书评

暂无评论

信息网络安全 2022年第5期 11-20页

作者：华景煜黄达明南京大学计算机科学与技术系南京210023

以太坊智能合约的形式化验证是目前的研究热点,在各种形式化验证方法中,定理证明方法具有误报少、可以处理大状态空间等优点。定理证明需要强大的形式化规约表达能力作为基础。文章对现有以太坊智能合约的定理证明研究中使用的形式化规... 详细信息

以太坊智能合约的形式化验证是目前的研究热点,在各种形式化验证方法中,定理证明方法具有误报少、可以处理大状态空间等优点。定理证明需要强大的形式化规约表达能力作为基础。文章对现有以太坊智能合约的定理证明研究中使用的形式化规约表达方法进行综述,从智能合约开发语言和区块链内生语义的建模、智能合约安全属性和功能属性的形式化规约表达、自动定理证明和交互式定理证明的选择等角度对形式化规约方法进行比较和讨论,并指出目前的困难和未来的研究方向。

关键词：以太坊智能合约形式化规约形式化验证定理证明

基于定理证明器HOL4的模糊控制器形式化研究

在线全文

学校读者我要写书评

暂无评论

基于定理证明器HOL4的模糊控制器形式化研究

作者：张展豪北京化工大学

学位级别：硕士

相较于传统控制方法,模糊控制能够有效处理复杂系统中存在的不精确性问题,从而得到了广泛应用。随着其应用范围的不断扩大,基于模糊控制的被控系统安全性就显得尤为重要;而传统的测试方法由于无法覆盖所有输入空间,因此不能确保结论的... 详细信息

相较于传统控制方法,模糊控制能够有效处理复杂系统中存在的不精确性问题,从而得到了广泛应用。随着其应用范围的不断扩大,基于模糊控制的被控系统安全性就显得尤为重要;而传统的测试方法由于无法覆盖所有输入空间,因此不能确保结论的完备性;为了将形式化验证方法引入基于模糊控制的应用验证中,保证其结论对于任意输入均成立,建立一个可复用的模糊控制器形式化模型是必不可少的工作。为此,本课题采用了形式化方法中的定理证明方法,基于HOL4(Higher-Order Logic4)对模糊控制器进行形式化研究。论文首先介绍了模糊数学中基础理论的形式化建模,其中包含了基本定义的形式化模型及其性质的验证,并将其表示为定理的形式;之后在此基础上设计了模糊控制器的形式化架构,主要包括四个模块的形式化建模及其整合;在建模过程中,模糊化方法函数、模糊子集、控制规则均作为参数输入,使模型具有更强的复用性;同时对模型中矩阵扩展为向量、规则库合成运算的功能函数在设计上进行了优化,降低了模型整体的复杂度;最后通过一个具体应用给出基于该设计的形式化验证过程;在验证中引入前向证明思想,规划关键的验证步骤,为目标中因嵌套递归而难以化简的问题提供了一种解决思路。本课题使用定理证明法,对模糊数学以及模糊控制进行了形式化研究,给出了模糊控制器的一种可复用形式化模型架构,扩展了定理证明法的应用范围,对未来使用定理证明法,验证以模糊数学及模糊控制为基础的算法具备一定的参考和借鉴价值。

关键词：模糊数学模糊控制形式化方法定理证明 HOL4

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

机械化定理证明研究综述

软件学报 2020年第1期31卷 82-112页

作者：江南李清安汪吕蒙张晓瞳何炎祥湖北工业大学计算机学院湖北武汉430068 武汉大学计算机学院湖北武汉430072

随着现代社会计算机化程度的提高,与计算机相关的各种系统故障足以造成巨大的经济损失.机械化定理证明能够建立更为严格的正确性,从而奠定系统的高可信性.针对机械化定理证明的逻辑基础和关键技术,详细剖析了一阶逻辑和基于消解的证明... 详细信息

随着现代社会计算机化程度的提高,与计算机相关的各种系统故障足以造成巨大的经济损失.机械化定理证明能够建立更为严格的正确性,从而奠定系统的高可信性.针对机械化定理证明的逻辑基础和关键技术,详细剖析了一阶逻辑和基于消解的证明技术、自然演绎和类型化的λ演算、3种编程逻辑、基于高阶逻辑的硬件验证技术、程序构造和求精技术之间的联系和发展变迁,其中,3种编程逻辑包括一阶编程逻辑及变体、Floyd-Hoare逻辑和可计算函数逻辑.然后分析、比较了各类主流证明助手的设计特点,阐述了几个具有代表性的证明助手的开发和实现.接下来对它们在数学、编译器验证、操作系统微内核验证、电路设计验证等领域的应用成果进行了细致的分析.最后,对机械化定理证明进行了总结,并提出面临的挑战和未来研究方向.

关键词：定理证明证明助手消解自然演绎类型化的λ演算编程逻辑求精

在线全文

学校读者我要写书评

暂无评论

约束求解与定理证明专题前言

软件学报 2023年第8期34卷 3465-3466页

作者：蔡少伟陈振邦王戟詹博华赵永望中国科学院软件研究所北京100190 国防科技大学计算机学院湖南长沙410073 浙江大学计算机科学与技术学院浙江杭州310007

随着计算机系统在工业和生活中越来越广泛的应用,软件和硬件的可靠性受到越来越多的关注.形式化方法使用严格的数学语言对计算机系统建模,并在计算机的辅助下验证系统的正确性.与测试不同,形式化方法可以完全排除某些类型的错误.约束求... 详细信息

随着计算机系统在工业和生活中越来越广泛的应用,软件和硬件的可靠性受到越来越多的关注.形式化方法使用严格的数学语言对计算机系统建模,并在计算机的辅助下验证系统的正确性.与测试不同,形式化方法可以完全排除某些类型的错误.约束求解和定理证明是形式化方法中的两大关键技术.在约束求解方面,SAT和SMT求解器已经在学术界和工业界得到了广泛应用,比如SAT求解器用于EDA领域的等价性验证,SMT求解器用于程序验证和白盒模糊测试等.交互式定理证明通过人和计算机之间的交互完成证明,能够验证非常复杂的系统和性质,例如编译器和操作系统的正确性验证.约束求解与定理证明专题关注约束求解和定理证明的理论、技术、工具与应用,包括在EDA、符号执行、模型检测、程序分析与验证、系统安全等领域的应用.

关键词：形式化方法定理证明约束求解符号执行计算机系统模糊测试模型检测系统安全

在线全文

学校读者我要写书评

暂无评论

半扩展规则下分解的定理证明方法

软件学报 2015年第9期26卷 2250-2261页

作者：张立明欧阳丹彤赵毅吉林大学计算机科学与技术学院吉林长春130012 符号计算与知识工程教育部重点实验室(吉林大学) 吉林长春130012 吉林大学电子科学与工程学院吉林长春130012

基于扩展规则的定理证明方法在一定意义上是与归结原理对偶的方法,通过子句集能否推导出所有极大项来判定可满足性.IER(improved extension rule)算法是不完备的算法,在判定子句集子空间不可满足时,并不能判定子句集的满足性,算法还需... 详细信息

基于扩展规则的定理证明方法在一定意义上是与归结原理对偶的方法,通过子句集能否推导出所有极大项来判定可满足性.IER(improved extension rule)算法是不完备的算法,在判定子句集子空间不可满足时,并不能判定子句集的满足性,算法还需重新调用ER(extension rule)算法,降低了算法的求解效率.通过对子句集的极大项空间的研究,给出了子句集的极大项空间分解后子空间的求解方法.通过对扩展规则的研究,给出了极大项部分空间可满足性判定方法 PSER(partial semi-extension rule).在IER算法判定子空间不可满足时,可以调用PSER算法判定子空间对应的补空间的可满足性,从而得到子句集的可满足性,避免了不能判定极大项子空间可满足性时需重新调用ER算法的缺点,使得IER算法更完备.在此基础上,还提出DPSER(degree partial semi-extension rule)定理证明方法.实验结果表明:所提出的DPSER和IPSER的执行效率较基于归结的有向归结算法DR、IER及NER算法有明显的提高.

关键词：定理证明命题逻辑扩展规则可满足性问题

在线全文

学校读者我要写书评

暂无评论

MSVL程序的自动定理证明方法

西安电子科技大学学报 2016年第1期43卷 75-81页

作者：马倩段振华西安电子科技大学计算理论与技术研究所陕西西安710071

时序逻辑程序设计语言能被用于验证C、Verilog/VHDL程序的正确性.但目前时序逻辑程序设计语言程序只能纯手工进行定理证明.针对该问题提出了一种基于定理证明器原型验证系统的时序逻辑程序设计语言程序的自动定理证明方法.该方法首先使... 详细信息

时序逻辑程序设计语言能被用于验证C、Verilog/VHDL程序的正确性.但目前时序逻辑程序设计语言程序只能纯手工进行定理证明.针对该问题提出了一种基于定理证明器原型验证系统的时序逻辑程序设计语言程序的自动定理证明方法.该方法首先使用原型验证系统规范语言描述时序逻辑程序设计语言的语法和语义,使得原型验证系统能够正确识别时序逻辑程序设计语言程序;然后使用原型验证系统规范语言描述时序逻辑程序设计语言的公理系统和待证定理;最后输入原型验证系统命令调用原型验证系统证明器来进行时序逻辑程序设计语言程序的推演证明.在证明过程中,细节被原型验证系统自动地证明,使得人工仅在复杂的步骤上指导控制,从而实现半自动地验证时序逻辑程序设计语言程序,简化了该定理的证明过程.

关键词：时序逻辑公理系统定理证明验证

在线全文

学校读者我要写书评

暂无评论

基于本体与Prolog的平面几何定理证明

电子科技大学学报 2011年第3期40卷 429-434页

作者：钟秀琴符红光丁盘苹电子科技大学计算机科学与工程学院成都610054

基于本体理论、本体模型等方面的研究,以一个平面几何定理证明问题为例,详细地描述了平面几何本体的构建过程、基于本体和Prolog规则的推理,及其在平面几何问题求解中的应用。实验结果表明,将本体应用于几何定理机器证明是一种行之有效... 详细信息

基于本体理论、本体模型等方面的研究,以一个平面几何定理证明问题为例,详细地描述了平面几何本体的构建过程、基于本体和Prolog规则的推理,及其在平面几何问题求解中的应用。实验结果表明,将本体应用于几何定理机器证明是一种行之有效的方法,该方法避开了以往的代数方法中多次反复判断的问题,更接近自然语言的描述,能明确地表达领域知识和实现概念分层,从而能快速地构建几何模型,还可以进行复杂关系间的推理,最终实现基于本体和Prolog规则的平面几何定理证明。

关键词：平面几何本体 Prolog RDF(S) 定理证明

在线全文

学校读者我要写书评

暂无评论

定理证明器Coq与机械语义研究

计算机应用与软件 2015年第10期32卷 10-14页

作者：窦亮刘强杨宗源华东师范大学计算机科学技术系上海200241

随着证明理论和定理证明器的不断发展与成熟,形式语义研究已经从传统的基于手工证明的研究进入到机器可处理的机械语义的研究。交互式定理证明器Coq具备强大的描述能力,可以形式化地描述程序语法和语义,利用其内置函数式编程语言实现对... 详细信息

随着证明理论和定理证明器的不断发展与成熟,形式语义研究已经从传统的基于手工证明的研究进入到机器可处理的机械语义的研究。交互式定理证明器Coq具备强大的描述能力,可以形式化地描述程序语法和语义,利用其内置函数式编程语言实现对程序语义的复杂操作,通过其证明系统形式地证明操作的正确性。根据形式语义的理论,针对简单类型Lambda演算的操作语义和指称语义,展示了如何利用定理证明器Coq的归纳定义实现它们的形式描述,并对语义的重要属性进行证明,表明机械语义是确保基础软件正确性的基础。

关键词：定理证明形式语义 Lambda演算机械语义