一种含等词的分阶段Tableau算法

在增强新的扩展规则的tableau方法的基础上提出了一种新的含等词tableau算法—分阶段tableau。在该算法中，将tableau四分成两个阶段，等词单独处理，利用提取不等式析取并在启发式的帮助下计算等价类的方法，进一步限制了tableau的搜索空间，提高了tableau的推理效率。同时，为了研究分阶段tableau的有效性，进行了实例分析，并与Fitting和Jeffrey方法进行了比较，结果表明，分阶段tableau方法优于其它方法。     

一种逻辑强化学习的tableau推理方法

tableau方法是一种具有较强的通用性和适用性的推理方法，但由于函数符号、等词等的限制，使得自动推理具有不确定性，针对tableau推理中封闭集合构造过程具有盲目性的问题，提出将强化学习用于tableau自动推理的方法，该方法将tableau推理过程中的逻辑公式与强化学习相结合，产生抽象的状态和活动，这样一方面可以通过学习方法控制自动推理的推理顺序，形成合理的封闭分枝，减少推理的盲目性；另一方面复杂的推理可以利用简单的推理结果，提高推理的效率。     

自由变量语义tableau中δ-规则的一种改进方法

自动推理一直是人工智能领域研究的重要内容．近几年来,由于tableau方法的通用性和直观性,引起人工智能界的广泛关注．对于自由变量语义tableau中的量词规则,由于r-规则替换的任意性,可导致在同一tableau证明中r-规则被多次使用,使得tableau推理结构树中出现多个自由变量．针对tableau中多次出现自由变量,使tableau封闭延迟的问题,在δ^ -规则的基础上,提出对δ^ -规则改进的δ^ -规则,并进行了正确性证明．将δ^ -规则应用到TableauTAP系统中,结果表明,δ^ -规则使tableau封闭提前,在推理的时间效率和空间效率上都有较大的提高．     

基于语义tableau的一阶逻辑自动定理证明

自动推理作为自动定理证明的扩展是人工智能研究的基础工作,许多重要的人工智能系统都是以推理系统为其核心部分,其中的tableau方法,由于具有通用性、直观性及易于计算机实现等特点,至今成为重要的自动推理方法之一。在tableau方法基础上,讨论了一阶逻辑中的自动定理证明理论,提出使用模型存在定理证明其可靠性和完备性的方法。同时也给出了带等词tableau方法的证明过程。     

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

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

一种基于语义tableau的数据库修正方法

tableau作为自动推理的有效方法之一在许多人工智能领域中有重要的应用。在tableau基础上，提出新的tableau开放和封闭的推理标准，应用于数据库实例不满足完整性约束的不相容关系数据库中，并对其进行修正。这样可以采用逻辑程序的方法，对数据库进行修正，解决了传统修正方法丢失信息、出现新的不相容等问题。     

MPI程序中通信原语转换方法研究

在当前存在的大量非结构化MPI程序中，许多基于点对点通信原语的代码段可以替换为相应的结构化集合通信原语，在MPI代码结构分析的基础上提出了一种MPI程序中点对点通信原语到集合通信原语转换的方法，首先分析非结构化MPI代码的内部结构，建立Diophantine不等式系统，然后用Omega库运算得到点对点通信代码段的通信模式集，再辅以数据交换分析确定对应的集合通信原语并替换，并给出了相应的实例分析。     

全变差图像恢复的交替方向乘子法

针对图像恢复的全变差（TV）模型提出了一种基于交替方向乘子法的快速求解算法。通过变量替换将TV模型转化为与之完全等价的等式约束优化问题,然后用交替方向乘子法求解等式约束优化问题。实验结果表明,相对于FTVd方法,克服了FTVd方法的不稳定性,视觉效果更好,信噪比也得到了提高。     

基于合一替换推理的密码协议分析

提出了一种简单的，更适合于自动化操作的密码协议分析方法，通过进一步分析攻击者的计算能力，形成一个有效的自动推理系统。攻击者为应答挑战主体的消息。把该消息应答转化为利用推理系统进行合一替换。并分别给出了Needham-Schroede协议的推理说明。     

翻译成整数规划的IP-tableau方法

由经典命题公式对应着0-1-整数规划的事实,提出将tableau方法与整数规划相结合的IP-tableau方法,并提升到一阶逻辑、多值逻辑以及无穷值逻辑。将tableau转化为IP方法后,可以采用许多提高IP效率的方法。另外在多值逻辑中,随着n值的增加,IP问题不会变得更加复杂。     

Connection Tableaux with Lazy Paramodulation

It is well known that the connection refinement of clause tableaux with paramodulation is incomplete (even with weak connections). In this paper, we present a new connection tableau calculus for logic with equality. This calculus is based on a lazy form of paramodulation where parts of the unification step become auxiliary subgoals in a tableau and may be subjected to subsequent paramodulations. Our calculus uses ordering constraints and a certain form of the basicness restriction.     

The Disconnection Tableau Calculus

In this paper we give a comprehensive presentation of the disconnection tableau calculus, a proof method for formulas in classical first-order clause logic. The distinguishing property of this calculus is that it uses unification in such a manner that important proof-theoretic advantages of the classical (i.e., Smullyan-style) tableau calculus are preserved, specifically the termination and model generation characteristics for certain formula classes. Additionally, the calculus is well suited for fully automated proof search. The calculus is described in detail with soundness and completeness proofs, and a number of important calculus refinements developed over the past years are presented. Referring to the model-finding abilities of the disconnection calculus, we explain the extraction and representation of models. We also describe the integration of paramodulation-based equality handling. Finally, we give an overview of related methods.     

A Goal-Type Driven Method of Solving Horn Logic with Equality

A new method of solving Horn logic with equality,the goal-type driven method,is presented,which considers explicitly the unification operator as a gloal and merged it into the resolution process,The metho has the following advantages.The resolution and the unification have been integrated in a uniform way.The architectures of the inference engines based on Horn logic with equality are simplified,Any techniques of exploiting AND/OR parallelism to solve goals can also be applied to unification at the same time.The method can be used to integrate the styles of functional language and logic language by a uniform framework.It can also deal with infinite data structures.     

What You Always Wanted to Know about Rigid E-Unification

This paper solves an open problem posed by a number of researchers: the construction of a complete calculus for matrix-based methods with rigid E-unification. The use of rigid E-unification and simultaneous rigid E-unification for such methods was proposed by Gallier et al., in 1987. After our proof of the undecidability of simultaneous rigid E-unification in 1995. (Degtyarev and Voronkov, 1996d), it became clear that one should look for more refined techniques to deal with equality in matrix-based methods. In this article, we define a complete proof procedure for first-order logic with equality based on an incomplete but terminating procedure for rigid E-unification. Our approach is applicable to the connection method and the tableau method and is illustrated on the tableau method.     

Adding equality to semantic tableaux

An extension to the system of semantic tableaux to deal with first-order logic with equality is introduced and proved sound and complete. This involves the use of partial unification, an operation which is based on unification without the presence of variables. We show, further, that semantic tableaux with partial unification provide a sound and complete proof method without needing the functionally reflexive axioms. We also give an example of an ordering rule which allows us to provide less complex proofs in the ground case.     

Tableau Methods for a Logic with Term Declarations

We study free variable tableau methods for logics with term declarations. We show how to define a substitutivity rule preserving the soundness of the tableaux and we prove that some other attempts lead to unsound systems. Based on this rule, we define a sound and complete free variable tableau system and we show how to restrict its application to close branches by defining a sorted unification calculus.     

A theory of complete logic programs with equality

Incorporating equality into the unification process has added great power to automated theorem provers. We see a similar trend in logic programming where a number of languages are proposed with specialized or extended unification algorithms. There is a need to give a logical basis to these languages. We present here a general framework for logic programming with definite clauses, equality theories, and generalized unification. The classic results for definite clause logic programs are extended in a simple and natural manner. The extension of the soundness and completeness of the negation-as-failure rule for complete logic programs is conceptually more delicate and represents the main result of this paper.     

一种基于集合符号的自动推理扩展方法

在多值逻辑Tableau推理的基础上,提出了一种基于集合符号的自动推理扩展方法.将符号集合作为真值,减少了Tableau的推理分枝,并可以将适合经典逻辑的推理方法和策略应用于其中,使得非经典逻辑推理经典化.使用SWI-PROLOG语言设计实现了基于集合符号的自动推理系统,在系统中使用集合符号方法,只需要在规则库中增加推理规则,即可生成规则程序,系统本身不需要任何的修改,因此一些适合于经典逻辑的推理方法和技巧就可以很容易地应用到多值逻辑、模态逻辑、直觉逻辑等非经典逻辑,也可以进一步推广到无穷值逻辑和含模糊量词(如T-算子和S-算子)的逻辑中,对于无穷值逻辑和模糊逻辑的Tableau方法研究具有一定的借鉴作用.对TPTP中的900个逻辑问题进行了证明,实验结果表明,系统在时间和空间上效率都是较高的.