数学史视角下正弦定理的证明

正弦定理是平面几何学的基本定理,文章从不同角度出发,按数学史时间的顺序,介绍16种证明方法,从最初的同径法到外接圆法,再到近现代的各种巧妙证法,从不同的证明方法中回顾正弦定理的发展史,通过对不同方法的分析比较,展现数学知识之间的联系,体现数学的美.

柯西中值定理的证明及其应用探索

为促进高职学生深入理解柯西中值定理的内容及应用,探索了两种证明柯西中值定理的方法,并阐释了三个中值定理之间的关系.介绍了柯西中值定理在等式证明、不等式证明、函数单调性判断及极限计算中的应用,并进一步应用柯西中值定理证明了洛必达法则、积分中值定理及泰勒定理.对柯西中值定理的证明、内涵及其在解题中的应用进行探索,为微分中值定理的学习和应用提供参考.

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

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

平面上Clifford定理的一般证明

Clifford定理作为几何学的一个最基本定理有着广泛的应用,读者通过该定理可以从整体上提高对几何学的认识。学习Clifford定理须从其证明入手,然而,目前很难找到一个通俗且完整的证明。文章利用实交比值引理给出了平面上Clifford定理的一般证明,这一方法对任意n条一般直线都适用。

Clifford代数与几何定理机器证明

Clifford代数是一种深深根植于几何学之中的代数系统。近年来 ,它在微分几何、理论物理、经典分析等方面取得了辉煌的成就 ,是现代理论数学和物理的一个核心工具 ,并在现代科技的各个领域 ,如机器人学、计算机视觉等方面有广泛的应用。本文主要介绍Clifford代数在数学机械化的核心内容—几何定理机器证明中的应用。作为一种非常优秀的描述和计算几何问题的代数语言 ,Clifford代数对于几何体 ,几何关系和几何变换有不依赖于坐标的、易于计算的多种表示 ,因而应用它进行几何自动推理 ,不仅使困难定理的证明往往变得极为简单 ,而且能够解决著名的数学公开问题。目前在国际上 ,几何自动推理已经成为Clif ford代数的一个重要应用领域。

复Clifford代数周期性定理的一个证明

在近代微分几何和数学物理的研究领域中 ,Clifford代数起着越来越重要的作用。关于Clifford代数 ,LawsonHB和MichelsohnML在他们的专著中做了一定的研究 ,得出了Clifford代数中的周期性同构现象。本文作者在复Clifford代数中引进超结构的概念 ,给出了复Clifford代数周期性定理的一个新的证明。

初等几何定理证明的Clifford代数方法

本文结合是吴方法及平面几何的Ｃｌｉｆｆｏｒｄ代数表示，提出了几何定理机器证明的一种完备的方法，用这种方法证明定理时，三角化的过程及证明的过程通常较以前的方法更简短而且它们是可以几何解释的。

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

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

多项式插值余项定理的一个自然证明

通过对插值多项式函数性质进行分析,多项式插值余项的基本形式得到诱导,再从该基本形式出发,获得了多项式插值余项定理的新证明.整个证明过程无需借助辅助函数的构造,因而显得较为自然.这种自然证明的方式也可用于Hermite切触型插值多项式余项的证明.

平面上的Clifford系列定理

Clifford定理的证明难度较大,尤其用初等几何学的方法来证明难度更大,至今没有发现一个较完整的用初等几何学的方法证明这一定理。文章利用实交比值引理给出了当n=4,5时的Clifford定理的证明。

综述中学勾股定理的证明方法

为了使中学生能高效解答勾股定理的题目,教师可以通过赵爽弦图证明、等面积、欧几里得证明和反证法等证明方法,使中学生更好地理解和掌握勾股定理的概念与本质。在日常的教学中,教师不断帮助学生理解勾股定理的证明,可以使学生更快和更熟练地运用勾股定理解决实际问题。

用搭积木的方法证明费马大定理没有正整数解

本文用搭积木的方法证明an+bn=cn,当n≧3时没有正整数解。

温故建构新知 论证生成巧思——三角形中位线定理的探究

平行四边形的对角线互相平分是三角形中位线定理的最近知识生长点,由此引出三角形中位线定理的概念并建构模型探讨不同视角下的论证方法,最后通过古题新做打破学生固有思维,完成对新知的吸收和内化,使学生的探究水平和知识的迁移能力得到稳步提升.

美国和英国早期教科书中的圆幂定理

选取1829—1948年间出版的80种美国和英国早期的几何教科书,探究其中关于圆幂定理的内容.研究发现教科书中推导相交弦定理、割线定理和切割线定理的各种方法,以及圆幂定理在数学内部和数学外部的应用,期望相关观点和素材能为圆幂定理的教学提供有益的参考.

基于Coq的RVWMO加载值公理形式化描述与推论证明

RISC-V内存一致性模型(RVWMO)规定了RISC-V多核系统的访存序约束,是RISC-V软硬件设计者共同遵守的重要规范,旨在为硬件设计提供灵活性的同时保证软件的易开发性。RISC-V指令集规范使用全局访存序、保留程序序以及三条公理(加载值公理、原子公理与进度保证公理)描述RVWMO。通过运用RVWMO的规则,可对多线程程序的访存序合法性进行判定,进而指导芯片设计、验证与软件开发。其中,加载值公理是最为复杂和难以运用的规则之一,是多个典型案例合法性判定的重要基础。然而,规范对于该公理的描述及案例讲解主要基于自然语言,缺乏清晰严格的形式化描述和推理过程,不利于读者理解和运用该公理。本文基于交互式定理辅助证明工具Coq,给出了RVWMO加载值公理的形式化描述以及相关引理、定理和推论的证明,对于理解运用RVWMO加载值公理和判定访存序的合法性具有重要意义。

展方法、品文化,让经典熠熠生辉——以《勾股定理》第一课时教学为例

1“勾股定理”探索的路径分析1.1路径比较《勾股定理》在人教版、苏教版、北师大版教材中均单列为一章,在章头图中或用2002年国际数学家大会会标图——赵爽弦图、或用与“外星人”联系的信号图形直观地揭示出勾股定理本质内涵与文化价值.在上述教材第一课时中基本上以“设置情境、操作测量、思考猜想、归纳证明”等环节呈现出“勾股定理”探索的路径,精彩纷呈.

运用定理证明器ACL2验证机器人操作系统ROS节点间通信

作为一种开源的机器人操作系统,ROS在家用或服务性机器人上也得到广泛应用,保证其设计的正确性相当重要.本文通过定理证明的方法对ROS的节点间通信进行形式化建模与属性验证.对通信层的节点间连接建立和消息传递过程进行抽象建模,模型融合网络拓扑、主题匹配和路由机制等部分,定义函数对其进行描述,提取路由函数的存在性、可达性及正确性等3个关键属性,运用定理证明工具ACL2对ROS节点间通信的功能正确性进行自动验证,证明消息从源节点出发并选择有效的传输路径到达目的节点.这种满足属性要求的参数化模型具有一般性和易扩展性,并能保证ROS节点间通信的终止属性和功能正确性,可为ROS通信层设计的正确性验证工作提供一个有效的方法参考.

运用定理证明的形式化方法验证SpaceWire编码电路

我国空间太阳望远镜(SST)项目采用了SpaceWire作为传输总线,目前针对SpaceWire总线的验证主要采用测试和模拟等传统的方法,这类验证方法是不完备的.本文旨在对SST项目中SpaceWire总线的DS编码电路是否如实地实现标准中的规范要求进行验证,运用定理证明的形式化方法,在HOL4工具上对该电路的设计实现与规范要求的一致性进行验证,克服了传统验证方法的局限性.

几何定理可读证明的自动生成

用计算机能生成几何定理的易为人们理解的证明吗？这个几十年来进展很小的难题，自１９９２年以来有了突破性进展．对于一大类欧氏几何命题──构造性几何命题，已有了相当有效的算法．基于此算法所编制的程序，已证明了５００多条非平凡的几何命题．对其中大多数命题，机器自动生成的证明是简明而易于理解的．本文是对这一领域近三年来取得的进展的综述．包括了在非欧几何可读证明方面的最新成果．

一种新的基于扩展规则的定理证明算法

基于扩展规则的定理证明方法是一种与归结方法互补的新的定理证明方法.首先通过对扩展规则的深入研究,给出了扩展规则的一个重要性质,设计并实现了该性质的判定算法.此外,从理论上分析及证明了该判定算法的时间和空间复杂性.基于此,提出了一种新的基于扩展规则的定理证明算法NER,将判定子句集可满足性问题转化为一系列文字集合的包含问题,而非计数问题.实验结果表明,算法NER的执行效率较原有扩展规则算法IER和基于归结的有向归结算法DR有明显提高,有些问题可以提高两个数量级.