质点法机器证明视角下的近世几何研究

优化并发展了质点法机器证明算法的核心程序,用Mathematica创建了新的几何定理证明器。拓展了机器证明的研究范畴,首次实现了近世几何的机器证明,且可读性令人满意。在该证明器的帮助下,发现了一些新的近世几何性质,深化了近世几何的研究成果,并对已有的近世几何研究成果提出一些意见。

基于定理证明器的行波进位加法器开发以及新的芯片设计方法探索

数字芯片的规模已经进入几百亿晶体管的时代,传统的硬件设计方法难以应对日益复杂的电路需求,比如基于Verilog语言的硬件设计。针对这个问题,文章以行波进位加法器为例,探索基于交互式定理证明器Coq的芯片设计方法,该方法不仅在Coq中完成了加法器的RTL描述,而且进行了加法器的功能仿真、形式验证、Verilog代码生成、网表生成和网表仿真。这个案例在单一的编程平台里把RTL设计同前端EDA的主要流程整合在一起,虽然案例简单,但可以初步体现出基于Coq的芯片前端设计的可能性,并且希望能够从此出发探索出新的基于定理证明器的芯片设计流程。文章的主要技术路线是在Coq中开发芯片设计的抽象语法树,然后基于这个抽象语法树展开行波进位加法器的前端开发流程。实验结果表明,Coq在支撑芯片设计方面有巨大的潜力,并且基于定理证明器的验证是可以复用的,这有利于验证大规模的系统。尽管这一方法处于探索阶段,但它为未来的芯片前端设计提供了全新的思路,有希望发展成为一种新型的芯片前端设计方法。

基于Isabelle定理证明器算法程序的形式化验证

形式化验证对保证软件的正确性和可靠性具有十分重要的意义。定理机械证明是形式化验证的一个重要研究领域,Isabelle系统是一个被广泛运用的定理证明辅助工具。本文在分析Dijkstra最弱前置谓词理论的基础上,根据PAR方法开发的算法程序循环不变式,提出了一种使用Isabelle定理证明器对算法程序进行机械验证的方法。该方法既克服了传统手工验证过程的繁琐性和易错性等缺点,又达到"提高验证效率和保证算法程序高可信"的目标,具有很好的实用价值。

内含定理证明器的程序开发系统

提出了一个基于重写技术的程序开发系统，它提供了扩展的函数式语言和代数规约语言相结合的混合语言，该语言中引入了优化规则和测试等式说明机制．优化规则用于优化代码和满足某些特殊需求．运用测试等式说明机制可使程序员在程序中给出一些用于测试的等式，对程序进行测试，这些测试是在被开发系统形成前进行的．对优化规则和测试等式的证明，是由系统中的证明子系统（定理证明器）完成的．定理证明器的引入，提高了所开发系统的正确性，并且有利于缩短系统的开发周期．

一个用于指针程序验证的自动定理证明器的设计与实现

对高可信软件需求的增加使得指针程序的验证成为近期的研究热点.指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析.介绍一个针对指针逻辑的自动定理证明器的设计和实现,描述了一些算法.实验结果表明,该定理证明器可以完全自动的证明用类C语言编写的关于单链表,双链表和二叉树的指针程序的验证条件,并生成机器可检查的证明.

用于指针逻辑的自动定理证明器(英文)

提出了一种为指针逻辑设计定理证明器的新技术,该项技术主要是基于变换和替代,已在APL的工具中得以实现.APL自动定理证明器是完全自动的,且其产生的证明可以被有效地记录和检验.已使用关于单链表、双链表和二叉树的指针程序测试了该自动定理证明器.

一个定理证明检查器

介绍了一种新型的形式说明语言 PD_ Cal,该语言具有良好的表达能力以及丰富的类型 .通过对由该语言描述的定理证明过程进行类型检查 ,可判断该证明是否是给定定理的正确的证明 .在该思想的基础上 ,设计并实现了PD_ Cal定理证明检查器 .

基于重心坐标的平面几何证明器

证明平面几何问题,所选的参考坐标系对于问题的解决有重要的影响.基于重心坐标系解决平面几何问题的好处是方法简单,过程简洁,同时,有利于实现证明的机械化.将重心坐标作为算法,在Maple下编写的程序Gp可以高效地证明一类平面几何问题.

质点几何定理证明的机器实现

本文针对质点法生成的目标关系式的过程不简明,缺少明显几何意义的问题,提出了一种具有较高可读性算法的几何定理证明器MMP.首先,直接从消点公式推导目标关系式,该方法不再使用质点坐标而直接对质点进行运算;其次,利用三个模块架构证明器,形成了具有完全性的消点过程;最后,利用待定系数法判定结论语句.由于可以对点直接进行运算,该证明器的消点过程比原有质点法具有明显的几何意义和较高运算效率.

语义Tableau定理证明器的Prolog实现

语义Tableau是一种具有较强通用性和适用性的推理方法。基于Prolog语言,并利用语义Tableau方法,在M.C.Fitting提出的一阶逻辑自动定理证明器的基础上提出了一些改进,给出了改进后相应的算法,并且对算法的可终止性和正确性进行了证明。实验结果表明,优化后的语义Tableau定理证明器,大大提高推理效率。

LCL并网逆变器的自抗扰控制设计与仿真

并网系统是一个强不确定性和非线性的复杂系统,其控制方式直接影响并网系统能否安全、稳定、高质量运行。因此,基于LCL并网逆变器数学模型,设计一种三阶自抗扰电流控制器,通过四阶线性扩张状态观测器对系统的不确定性及扰动进行观测补偿,将被控对象还原为标准积分串联型。使用频率响应法详细分析系统的跟踪性和抗扰性,并通过李雅普诺夫稳定性判据证明了闭环系统是渐进稳定的。最后,搭建MATLAB仿真平台验证控制策略的有效性,结果表明,所设计的电流控制策略提高了并网电流质量、系统的鲁棒性和控制品质。

换热器数值计算中传热边界条件的设定

基于对换热器内流体流动通道间传热的热力学第一定律的分析 ,提出了换热器数值计算中传热边界条件的设定方法。通过对采用不同传热边界条件数值计算结果的对比分析 ,并与实验测试结果对比 ,证明该边界条件设定方法切实可行 ,而且可以提高计算结果可信度。

三元复合式消色差补偿器的研究与测试

光学补偿器是一种光相位可在一定范围内连续可调的延迟器件,是偏光技术中的一个重要光学元件。对于三元复合式补偿器来说,只需转动其中的一个波片便可实现延迟量在0～2π之间连续可调,而且调节方便,调整量大,精度高。本文在复合式补偿器研究基础上,进一步从理论和实验上证明了该补偿器不仅具有相位补偿性能,而且在一定的光谱范围内满足消色差性能,削弱了延迟量对波长的依赖关系,适合于复色光使用。

具有在线提取器的成员基于身份的群签名方案

基于身份的群签名方案(ID-based GS)在本质上是追踪机制得到优化的群签名方案。ID-based GS方案的优势是对用户的成员公钥及其公开识别信息(如IP地址)进行了紧密的绑定。然而,已有的ID-based GS方案并不令人满意,这主要体现在无法在形式化的安全模型下得到证明,仅实现了放宽的安全性质,以及效率不高。通过结合双线性群上的消息块签名方案以及具有在线提取器的非交互知识证明技术,提出一个更为实用的ID-based GS方案。新方案具备两个显著的性质,即打开权威可以独立地打开争议的签名,而且注册协议能够以并发方式执行。此外,利用迭代散列函数和批验证技术,可以进一步地降低新方案的运算耗费。

标准模型下支持多协助器的强密钥隔离签名方案

并行密钥隔离签名方案通常允许2个协助器轮流帮助签名者进行临时私钥更新,然而当2个协助器密钥和任一临时私钥同时发生泄露时,伪造者则可以伪造任意时间段的签名.为了进一步提高签名方案的安全性,提出了一个新的支持n(n>2)个协助器的强密钥隔离签名方案.提出的方案中,即使用户的密钥更新频率增加为原密钥隔离系统的n倍,每个协助器密钥发生泄露的概率仍然与原密钥隔离系统相同,不会增加协助器密钥暴露于不安全环境的概率,从而减小了密钥泄露带来的危害.基于计算Diffie-Hellman假设,在标准模型下证明了方案的安全性.

定理证明辅助工具PVS剖析

ＰＶＳ是斯坦福研究机构开发的强大的规约、验证系统，它的适用领域广泛。在概要介绍ＰＶＳ的构成、功能后，着重分析了ＰＶＳ的规约语言、验证系统的特点，以及使得ＰＶＳ灵活、强大的设计决策和内在机制．

基于Z3的Coq自动证明策略的设计和实现

形式化验证方法被认为是一种构建高可信软件系统的有效手段.在定理证明工具通过手动写证明脚本来验证系统软件的功能正确性,这种验证方式表达力强,可以证明复杂系统,但是自动化程度低、验证代价比较高;而使用程序验证器接受经过规范标注的源代码生成验证条件,并将验证条件交给约束求解器自动求解,这种方式自动化程度高,缺点在于它很难验证复杂系统软件的全部功能的正确性.结合上述两种方式的优点,在定理证明工具Coq中实现了一个自动证明策略smt4coq,它通过在Coq中调用约束求解器Z3自动证明32位机器整数相关的数学命题,提高了自动化验证的程度,减少了用户手动验证程序的开销.

自动定理证明:十年回顾

本文主要介绍近十年来定理证明器的发展情况,同时讨论了与自动定理证明相关的一些问题。

μC/OS-Ⅲ任务调度器在Coq中的验证

以μC/OS-Ⅲ内核中的任务调度器为研究对象,选取调度相关的核心代码,验证调度器代码满足优先调度最高优先级任务的性质。基于分离逻辑与SCAP验证理论,利用Coq辅助证明工具,通过定义机器模型、操作语义、逻辑断言以及推导规则构建验证框架。在验证框架中,定义内核数据结构和内核相关性质的逻辑描述,模块化地对内核代码进行推理。验证结果表明,μC/OS-Ⅲ任务调度器满足可靠性要求,并且可以通过机器的自动检查。