二次多项式根的Schur-Cohn定理和Miller定理的初等证明

二次多项式根的大小在差分格式和系统的稳定性判定方面有着重要的意义.这里我们推荐有关的Schur-Cohn定理及其推广Miller定理,并给出初等证明. 考察二次多项式p(z)=az~2+bz+1(a≠0)的根z_1,z_2的模的大小.设z_1=     

时序逻辑程序的证明系统

本文为时序逻辑语言XYZ/E建立了一个证明系统.其主要特点是:1.证明可以直接在时序逻辑系统中进行,无需另行建立专门的公理系统;2.可建立一些元数学定理以简化证明过程;3.可在逐步求精的过程中边设计边证明正确性.     

维护的证明论系统

给定一阶语言及该语言的一个理论，假设需要在理论中添加一个与理论不和谐的语句，并要求保持理论的扩张是和谐的，就必须删除理论内的某些语句．删除理论中尽可能少的语句，即保留理论与需要添加语句和谐的一个极大子集，是构造理论扩张的一种方法．本文构造出了针对上述理论扩张的证明论．该证明论的可靠性及完全性刻划了一般形式的理论扩张与典型的理论扩张间的联系．对于命题逻辑，本文还给出了判定理论扩张的一种方法．     

六自由度运动系统运动范围的初等分析法

本文从运动学的观点出发,利用初等数学有关知识,对协同式六自由度运动平台的运动范围进行了分析,以运动平台升降、倾斜方向为例,给出了运动平台运动范围的求解方法。此种算法简单、实用,为初学者熟悉协同式六自由度运动平台的运动范围求解提供了一种简单易学的方法。     

可记忆交互式证明、零知识证明系统

交互式证明和零知识证明是现代密码学中非常重要的两个概念。自从它们被提出以来，在国际上受到了广泛的关注，许多学者投入到了这一领域的研究当中。同时，有越来越多的关于零知识的密码协议用于实际的电子商务及加密系统中。在我们的文章中，我们首先对图不同构问题的交互式证明和零知识证明两个协议进行了考察，并且发现两者在构造以及应用上都存在着本质的区别：前     

实初等与复初等函数之对比

本文是基于作者在高等数学和复变函数这两门课程教学过程中的一些思考,整理并总结了有关于大家熟知的初等函数在不同数学分支里的区别和联系,以便为后学者提供参考和借鉴.     

可行的证明整数是Blum数的零知识证明系统

Blum数是形如pk11qk21(p1和q1是模4余3的不同素数,且k1和k2是奇整数)的整数.目前,该类整数在密码学领域中得到了广泛的应用.尽管证明一个秘密整数是Blum整数的零知识证明系统已经存在,但是,怎样构造一个证明秘密整数是具有p1q1形式的Blum整数的零知识证明系统是未知的.基于Σ-协议,构造了证明秘密整数是具有p1q1形式的Blum整数的零知识证明系统,而且,也构造了证明秘密整数是具有pk11qk21(其中k1和k2至少有一个大于1)形式的Blum整数的零知识证明系统.     

基于能力系统的应用证明研究

通过对可信计算及其主要功能“远端证明”的分析，提出“应用证明”的概念及原理，并说明支持应用证明所需的安全机制。分析现有主流操作系统所使用的保护结构和访问控制模型，说明应用证明在当前的主流操作系统上是无法实现的。通过对能力系统EROS进行改进，使其充分支持应用证明，并提高系统的安全性及可信性。     

不可满足公式的同态证明系统

合取范式(CNF)公式H到F的同态φ是一个从H的文字集合到F的文字集合的映射,并保持补运算和子句映到子句.同态映射保持一个公式的不可满足性.一个公式是极小不可满足的是指该公式本身不可满足,而且从中删去任意一个子句后得到的公式可满足.MU(1)是子句数与变元数的差等于1的极小不可满足公式类.一个三元组(H,φ,F)称为的一个来自H的同态证明,如果φ是一个从H到F的同态.利用基础矩阵的方法证明了:一个不可满足公式F的树消解证明,可以在多项式时间内转换成一个来自MU(1)中公式的同态证明.从而,由MU(1)中的公式构成的同态证明系统是完备的,并且由MU(1)中的公式构成的同态证明系统与树消解证明系统之间是多项式等价的.     

基于能力系统的应用证明研究

通过对可信计算及其主要功能“远端证明”的分析,提出“应用证明”的概念及原理,并说明支持应用证明所需的安全机制。分析现有主流操作系统所使用的保护结构和访问控制模型,说明应用证明在当前的主流操作系统上是无法实现的。通过对能力系统EROS进行改进,使其充分支持应用证明,并提高系统的安全性及可信性。     

递归数据传送进程的证明系统

本文提出了递归数据传送进程互模拟的证明系统，并证明了其可靠性和相对于数据推理的完备性，其中关键的推理规则是唯一不动点归纳法，这个结果一方面将Ｍｉｌｎｅｒ关于正则基本ＣＣＳ的公理系统推广到数据传送进程，另一方面将Ｈｅｎｎｅｓｓｙ与Ｌｉｎ关于有穷数据传送进程的证明系统推广到无穷进程。     

哈希证明系统及应用研究

哈希证明系统在2002年欧密会上由Cramcr和Shoup首次提出。哈希证明系统的概念自提出以来得到广泛 研究,目前已有多个修改版本。“投影性”和“平滑性”是哈希证明系统的两个重要特性,正是由于这两个特性使得哈希 证明系统除了用于设计CCA安全的公钥加密体制之外,还广泛应用于各种安全协议设计,比如:基于口令认证的密钥 交换协议、不经意传输协议、可否认的认证协议、零知识证明协议和承诺协议等。介绍了哈希证明系统及其变形的各 种定义,分析了定义之间的派生关系和安全级别关系,并讨论了哈希证明系统在密码学中的应用.     

关于互连网络群论模型的一簇猜想

连通图生成的Cayley图是作为互连网络的群论模型提出来的概念。猜想:设G=(V,E)是具有顶点集{1,2,…,n}(n>2)和m条边的连通图。如果m=2r,则由G生成的Cayley图是边不交的k(0≤k≤r)个Hamilton图和m－2k个完美对集的并;如果m=2r+1,则由G生成的Cayley图是边不交的k(0≤k≤r)个Hamilton图和m－2k个完美对集的并。特别地,对于k=r和星网络,这个猜想的特殊情形是1998年由师海忠提出来的。     

一个出具证明编译器原型系统的实现

出具证明编译器是随着人们对现今的软件提出更高的可靠性和安全性要求而产生的工具,它结合了以往程序设计和程序安全性证明的技术。论文介绍了一个出具证明编译器原型系统的实现。     

重言衍推系统的试探法自动证明

提出针对重言衍推系统的模仿人类思维方式的生成可读证明的算法:试探法.试探法将待证的命题逐步分解成子命题并构造一颗证明树,对重言衍推系统中的定理证明取得了较好的效果.     

项重写系统等价性的归纳证明

尽管学者们在计算机软件理论及相关数学理论方面做出了不懈的努力,但伴随着计算机硬件的高速发展而来的软件危机却日益严峻,其原因复杂多样。其中,主要原因之一是缺乏程序验证的方法和工具。程序设计的主要步骤有:描述问题、设计程序、实现程序及测试程序。需要注意的是,这里是测试程序的正确性而非证明程序的正确性,这样程序的正确性就不能从根     

基于广义归结的定理机器证明系统

本文使用Ｃ—ＰＲＯＬＯＧ语言在ＳＵＮ工作站上设计实现了基于广义归结和基于归结的两个定理机器证明系统ＧＲＭ,ＲＭ,证明了《数学原理》中Ｐａｒｔ１：ｍａｔｈｅｍａｔｉｃａｌｌｏｇｉｃ中ＳｅｃｔｉｏｎＡ与ＳｅｃｔｉｏｎＢ中全部定理（３５０个）．讨论ＧＲＭ和ＲＭ的时、空复杂性,并在实现设计中提出新的全局调度策略及归结式的化简、排序策略,以单子句恒真、恒假的判断代替了广义归结中的自归结,实现了带ＯＣＣＵＲ检查的模式匹配．     

基于Tableau的定理机器证明系统TableauTAP

使用SWI-PROLOG语言在微机上设计实现了基于tableau的定理证明系统TabIeauTAP。该系统可以证明不含等词的经典逻辑公式童耋譬逻辑公式，通过预处理自动生成tableau规则，因此容易对其功能进行扩展。应用该系统对TPTP的400个逻辑问题进行证明，实验结果表明，TableauTAP在时间和空间效率上都是比较高的。     

双向推理系统在初等几何自动解题中的实现*

目前采用较多的初等几何自动推理方法是单向推理法（包括前向推理和后向推理）,探讨将前推法与后推法结合起来进行初等几何的推理。实践证明,对较为复杂的几何问题来说,采用这种方法可以显著提高推理效率。