复杂表达式推理在计算机自动推理系统中的研究

计算机自动推理和几何定理机器证明已经取得令人瞩目的成果,自动推理的软件也出现了很多。完善解决表达式的推理是数学定理机械化证明必须达到的目的,但是关于表达式的推理还缺乏研究,因为表达式的推理不同于一般信息的推理,它没有固定的格式,信息表述复杂。本文在之前研究工作的基础上,通过对表达式在推理时的特征分析,提出一种表达式推理的方法,是向这个方向的一个尝试。在该方法中,通过适当的替换,将表达式化为空,从而实现了表达式的简单处理,并在文中列举几个实例进行分析。实践证明,利用这种方法,可对大多数的结论为表达式的几何命题给出可读证明过程。     

几何信息压缩在计算机自动推理系统中的研究

着力于在推理系统中合理地组织几何信息的数据结构,提高推理的效率,减小算法的时间复杂度,对信息进行了描述,采用了等价类、角的压缩和归一化、信息组对等方法,阐述了几何信息在推理时压缩的实现,介绍了压缩信息的展开与提取技术,并通过计算机程序证明该类方法可以实现。实验结果表明,对较复杂的几何问题来说,采用这种方法可以显著提高推理效率。     

相干命题逻辑自然推理系统NR的自动证明*

给出了相干命题逻辑自然推理系统NR的自动证明算法。首先将待证命题公式A的子公式组成一个初始集合P,对其中的元素采用系统NR的推理规则得到新的命题公式加入P,当得到秩为0的A时命题得证;然后对A的证明树进行整理即得到演绎序列。对系统NR的大部分定理证明取得了良好的效果,算法生成的演绎序列清晰可读,接近手工推理。     

相干命题逻辑系统R的一种演绎生成算法

本文提出了相干命题逻辑系统R的一种演绎生成算法--试探法。该算法采用后向推理法,依据推理规则将待证命题逐步分解成子命题并构造一棵证明树,对系统R中的定理证明取得了较好的效果。     

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

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

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

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

基于拼凑替换的定理机器证明的研究与实现

机器定理证明可以避免人工证明容易出现的低级错误,是人工智能的重要方面,有广泛的应用前景;函数式程序设计的设计思想更加接近于数学,在定理证明方面有天然优势.人们证明逻辑推理的过程通过函数式程序实现,并将其证明的步骤显示出来,采用了逻辑推理机器证明.通过思考人脑在证明定理时的思考方式,给出了一个简单易懂的机器证明的方式.首先将证明的已知和结论形式化,将已知设为start,结果为end,已经证明的公理就是road,那么证明的过程就是从start沿着road到达end的过程.实验表明,逻辑证明通过函数式程序实现,达到了预期目的.     

自由选择工作流网的可靠完备化简规则集

流程化简技术是一种重要的商业流程模型分析方法.已有的非形式化化简方法因缺乏理论基础而无法保证完备性.基于Petri 网的化简方法应用范围不针对流程模型因而不能保证可靠性.提出了针对自由选择工作流网的一个可靠完备化简规则集,可靠性保证化简过程中这类模型的行为正确性被保持,完备性保证任意一个正确的此类工作流网最终都能被化简为最简形式.基于化简规则集给出可靠完备的合成规则集,用于流程模型的设计与精化.     

基于表达式的优惠模型研究

在业务运营支撑系统中,灵活的优惠策略是保障运营商针对客户的不同需求提供个性化服务的关键。在分析传统优惠策略不足的基础上,构建了四层优惠逻辑模型,引入了基于表达式的优惠函数。该模型能够提供丰富的优惠计算方法,以便运营商制定灵活的优惠策略,更好地实现“以客户为中心”的服务理念。验证表明：提出的基于表达式的优惠策略具有良好的灵活性、配置性和实用性。     

在计算机中实现三角函数的硬件解算方法

针对目标跟踪中大量存在的三角函数运算,提出在火控计算机中建立三角函数解算单元,采用硬件实现三角函数解算的设想。而三角函数解算单元是一种可以完成正弦函数解算功能的函数芯片。它的设计核心是以角度值为地址,通过硬件查表计算,可对0到90度的正弦函数值进行查表。查表精度可设计到0.001°,最大查表时间即为函数值的解算时间。余弦查表计算是采用正弦同一芯片,可以根据相位差90度的关系进行查表。实践表明三角函数的硬件解算速度快,精度高,可以替代通常方法的函数解算。因此,如果在火控系统中,设计一个地址译码器电路,就可建立多个三角函数芯片解算单元,通过计算机数据指令,实现对多个三角函数值的并行计算,从而提高系统对多个目标的快速跟踪处理能力。     

OTTER and the Moufang identity problem

This article provides additional evidence of the value of using an automated reasoning program as a research assistant. Featured is the use of Bill McCune's program OTTER to find proofs of theorems taken from the study of Moufang loops, but not just any proofs. Specifically, the proofs satisfy the property of purity. In particular, when given, say, four equivalent identities (which is the case in this article), one is asked to prove the second identity from the first, the third from the second, the fourth from the third, and the first from the fourth. If the proof that 1 implies 2 does not rely on 3 or 4, then by definition the proof is pure with respect to 3 and 4, or simply the proof is pure. If for the four identities one finds four pure proofs showing that 1 implies 2, 2 implies 3, 3 implies 4, and 4 implies 1, then by definition one has found a circle of pure proofs. By finding the needed twelve pure proofs, this article shows that there does exist a circle of pure proofs for the four equivalent identities for Moufang loops and for all orderings of the identities; however, for much of this article, the emphasis is on the first three identities. In addition — in part to promote the use of automated reasoning programs and to answer questions concerning the choice of options — featured here is the methodology that was employed and a discussion of some of the obstacles, some of which are subtle. The approach relies on paramodulation (which generalizes equality substitution), on demodulation, and — so crucial for attacking deep questions and hard problems — on various strategies, most important of which are the hot list strategy, the set of support strategy, and McCune's ratio strategy. To permit verification of the results presented here, extension of them, and application of the methodology to other unrelated fields, a sample input file and four proofs (relevant to a circle of pure proofs for the four identities) are included. Research topics and challenges are offered at the close of this article.This work was supported by the Mathematical, Information, and Computational Sciences Division subprogram of the Office of Computational and Technology Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

Human-oriented and machine-oriented reasoning: Remarks on some problems in the history of Automated Theorem Proving

Examples in the history of Automated Theorem Proving are given, in order to show that even a seemingly mechanical activity, such as deductive inference drawing, involves special cultural features and tacit knowledge. Mechanisation of reasoning is thus regarded as a complex undertaking in cultural pruning of human-oriented reasoning. Sociological counterparts of this passage from human- to machine-oriented reasoning are discussed, by focusing on problems of man-machine interaction in the area of computer-assisted proof processing.     

亲属关系的逻辑意义及其自动推理

用一阶谓词逻辑设计了一个亲属关系的自动推理模型。首先,把亲属关系（称谓）视为谓词,相关的人物视为变元,把亲属关系和有关性质用“或”、“与”及“逆”等运算符号联结成亲属关系表达式。然后,选取11种基本的亲属关系作为亲属基元,并构造亲属基元转换和化简的九大定理,用以描写和定义其他一百多种亲属关系,从而形成亲属关系转换的核心知识库。最后,给出一种简洁的亲属关系转换算法,主要包括连接、求逆、化简和组配等运算。     

三值关联规则在不确定性知识表示及推理中的应用

针对传统关联规则和 Ｂｏｏｌｅａｎ规则矩阵无法进行不确定性知识表示和推理的弱点,该文采用三值逻辑表示规则和真值状态的不确定性,提出并使用三值关联规则（Ｔ规则）和三值规则矩阵（ＴＲ矩阵）,利用 ＴＲ矩阵变换实现高速前向推理和后向推理。对复合三值规则的无损分解进行了详细探讨,最后提出了一个能进行不确定推理的新算法。     

BP神经网络结构参数的计算机自动确定

研究表明,由多层FNN的BP算法误差函数构成的非线性方程组的独立方程个数和FNN的待求未知变量的个数应该相等,该方程组才能有唯一组解。由此导出网络结构方程式,进而导出隐层层数判别式和每层神经元个数判别式。依据Kolmogorov定理,由该判别式得出求解FNN隐层层数和每个隐层神经元个数的具体算法。计算机仿真结果表明该方法简明实用。     

The combination of multiple classifiers using an evidential reasoning approach

In many domains when we have several competing classifiers available we want to synthesize them or some of them to get a more accurate classifier by a combination function. In this paper we propose a ‘class-indifferent’ method for combining classifier decisions represented by evidential structures called triplet and quartet, using Dempster's rule of combination. This method is unique in that it distinguishes important elements from the trivial ones in representing classifier decisions, makes use of more information than others in calculating the support for class labels and provides a practical way to apply the theoretically appealing Dempster-Shafer theory of evidence to the problem of ensemble learning. We present a formalism for modelling classifier decisions as triplet mass functions and we establish a range of formulae for combining these mass functions in order to arrive at a consensus decision. In addition we carry out a comparative study with the alternatives of simplet and dichotomous structure and also compare two combination methods, Dempster's rule and majority voting, over the UCI benchmark data, to demonstrate the advantage our approach offers.     

基于未知扰动的冲突证据合成方法

自从发现Dempster合成可能导致悖论以来,冲突证据合成一直是Dempster-Shafer理论的重要研究方向之一,迄今尚未有统一的解决方法被广泛接受.提出一种新的冲突证据合成方法,即在Dempster合成之前,基于未知扰动对mass函数进行预处理,并通过预处理来解决标准化问题.与其他相关方法相比,这种新方法不仅和Dempster规则形式上一致,合成过程比较灵活,并且可以通过扩展的Bayes公式得到理论上的解释.     

证据理论的主客观整合推理方法

现有证据理论研究侧重于从客观证据中提取证据源可靠性(RES)信息,而未考虑知识、经验、直觉等主观认知信息对RES推断及证据融合的积极作用。为此,基于证据距离和两两比较判断矩阵,提出反映证据源相对可靠性的主客观RES矩阵,以调节总误差最小为目标函数,构建用于提取证据源综合可靠性信息的RES整合模型,并结合Dempster组合规则给出证据推理步骤。数值实例验证了该方法的可行性。