一个有效的公开可验证的秘密共享方案

文献[1]首次提出的公开可验证的秘密共享方案在安全多方计算协议的设计中有重要作用,然而[1]提出的两个具体的方案在公开验证参与者收到共享的有效性时,需要进行大量的计算,因而是不实用的.本文提出一个共享给定公开值的秘密方幂的PVSS(SP-PVSS),该方案大大减少了共享有效性验证的计算量,具有更好的实用性.     

一种求解混合约束问题的快速完备算法

布尔与数值变量相混合的约束问题有着广泛的应用,但是当约束中的数值变量间存在非线性关系时该问题求解起来十分困难.目前的许多求解方法都是不完备的,即这些方法不能完全肯定某些包含非线性数值表达式的约束是否能够成立.针对这种问题,提出了数值与区间分析相结合进行数值约束求解的方法.已经实现了一个基于此方法的原型工具.实验结果表明,该方法能够有效、快速、完备地求解非线性混合约束问题.     

一类构造性几何不等式的机器证明

阐述了一个基于胞腔分解的不等式证明算法．据此算法编制的Maple通用程序能有效地处理含有根式的不等式型定理,对于Bottema等所著《几何不等式》一书中的大部分不等式定理的验证尤其高效．     

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

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

求解非线性区间数规划的微免疫优化算法研究

基于区间分析和免疫学原理,探讨非线性区间数规划问题解的概念和性质,以及求解的免疫优化方法和算法的理论基础.首先,基于该问题的最优值区间,给予最优解概念;研究区间值优化问题有效解的性质,探讨区间自然扩张规划与区间数规划的解之间联系,获得有效解是最优解的充分条件以及寻优的有效途径.其次,基于免疫应答的简化机制,设计具有群体规模小、可调参数少、结构简单等特点的非主从结构微免疫优化算法,并获证该算法具有收敛性和低计算复杂度.通过扩展标准测试函数和应用事例,比较性的数值实验结果显示,此算法执行效率高、搜索效果好,对低、偏高维非线性区间数规划具有较好应用潜力.     

面向对象编程与定量证明相结合实现问题自动求解

本文针对一类智能决策支持系统中，基于模型行为仿真以实现解题过程自动化的需要，提出对模型对象行为的一阶词演算型表达和面向对象型模型处理过程的形式化体系。将问题自动求解过程转化为逻辑运算问题，通过归结反演求取问题的解。文中给出一个应用实例。     

常用基本不等式的机器证明

不等式机器证明问题是智能系统领域的难点和热点问题.借助不等式证明软件BOTTEMA,对若干常用的基本不等式成功地实现了机器证明,包括算术、几何与调和平均不等式、排序不等式、Chebyshev不等式、Bernoulli不等式、三角形不等式及Jensen不等式等.所论不等式含有的变元个数是一个不确定的变量,属于Tarski模型外的不等式类型.机器证明得出的结论有时可能是已知结果的推广,其方法本身对同类不等式有示范性,更多的例子表明了该算法和软件的有效性.     

MSP问题的一个求解算法

MSP问题是文献［1,2］提出的一个问题。研究表明［3］该问题对NP类问题有很强的表达能力。本文给出一个关于该问题的求解算法、复杂性分析,以及正确性证明。本文对于NP完全问题研究有重要意义。     

非线性方程求解的泛灰数学方法

在概述泛灰数的概念及其运算规则的基础上,介绍了泛灰数与区间数的转化,利用泛灰数的可扩展性对区间进行分析.根据对求解区间的泛灰函数性质(如果在区间上有解,则0∈F(X))进行判定是否有解,剔除无解区间,细化有解区间,从而求解非线性方程的全部解.泛灰数不仅具有区间分析功能,且能解决区间分析所不能解决的问题.基于泛灰数的性质提出了求解非线性方程的一种新方法.算例证明了算法的有效性,该方法已成功地用于求解机构学问题.     

区间非线性路径约束的动态优化问题求解

本文研究路径约束中含有区间参数形式的动态优化问题,提出了一种新的非线性路径约束的确定化描述形式,和采用惩罚函数法的求解算法。对于转化后的极大极小优化命题,论文提出采用Lagrangian多项式加权和的方法得到有限维的确定性优化求解形式。该算法可有效地描述和求解不确定参数动态优化问题。     

Towards mechanical metamathematics

Metamathematics is a source of many interesting theorems and difficult proofs. This paper reports the results of an experiment to use the Boyer-Moore theorem prover to proof-check theorems in metamathematics. We describe a First Order Logic due to Shoenfield and outline some of the theorems that the prover was able to prove about this logic. These include the tautology theorem which states that every tautology has a proof. Such proofs can be used to add new proof procedures to a proof-checking program in a sound and efficient manner.     

支持用户自定义谓词的自动定理证明的研究

在先前设计的一个出具证明编译器原型基础上,增加了可用来描述数据结构性质的自定义谓词,对断言语言表达能力方面做了提升.在出具证明编译器的框架内,借助自动定理证明技术,针对自定义谓词的特点,设计了专门的推理规则,由此实现自定义谓词专用的自动定理证明器原型,并将它并入系统原来的自动定理证明器中.该原型可以用来证明操作单链表、二叉树等共享数据结构的程序的性质,其程序规范中可以使用自定义谓词描述数据有序性、链表长度等性质.     

A New Approach for Automatic Theorem Proving in Real Geometry

We present a new method for proving geometric theorems in the real plane or higher dimension. The method is derived from elimination set ideas for quantifier elimination in linear and quadratic formulas over the reals. In contrast to other approaches, our method can also prove theorems whose complex analogues fail. Moreover, the problem formulation may involve order inequalities. After specification of independent variables, nondegeneracy conditions are generated automatically. Moreover, when trying to prove conjectures that – apart from nondegeneracy conditions – do not hold in the claimed generality, missing premises are found automatically. We demonstrate the applicability of our method to nontrivial examples.     

Automatic Discovery of Theorems in Elementary Geometry

We present here a further development of the well-known approach to automatic theorem proving in elementary geometry via algorithmic commutative algebra and algebraic geometry. Rather than confirming/refuting geometric statements (automatic proving) or finding geometric formulae holding among prescribed geometric magnitudes (automatic derivation), in this paper we consider (following Kapur and Mundy) the problem of dealing automatically with arbitrary geometric statements (i.e., theses that do not follow, in general, from the given hypotheses) aiming to find complementary hypotheses for the statements to become true. First we introduce some standard algebraic geometry notions in automatic proving, both for self-containment and in order to focus our own contribution. Then we present a rather successful but noncomplete method for automatic discovery that, roughly, proceeds adding the given conjectural thesis to the collection of hypotheses and then derives some special consequences from this new set of conditions. Several examples are discussed in detail.     

程序规范自动检测与修正系统ADRS的研究

文中介绍了一个程序规范自动检测与修正系统ＡＤＲＳ的理论模型,在开放逻辑的思想基础上,文中提出了一种自动修正模型,并试图对李未提出的３个问题给出解决方案。作为对第１个问题的解决,作者提出了一种刻画程序规范重要性程度的全序结构,克服了加标记的二分法地粗糙性。作为对第２个问题的解决,作者提出了修正函数的定义和Ｒ－计算模型,并证明了该模型满足修正函数的要求。作为对第３个问题的解决,作者提出了Ｔ－修正函数的