U-循环项与易项*

本文引进了u-循环的概念，并证明了所有u-循环项都是易项．从而刻画了一类易项的归约性质，这对于研究停机问题具有相当意义．     

若干限制形式的缺少推理的复杂性

该研究判定一字是否出现在缺省理论〈Ｄ,Ｗ〉的某一扩张中的复杂性,其中,Ｄ是一种Ｈｏｒｎ缺省规则,而Ｗ是ｄｅｆｉｎｉｔｅ公式或Ｂｉ－Ｈｏｒｎ公式。     

一个带破圈启发方法的回答集编程系统

回答集编程(answer set programming,ASP)是一种回答集语义下的逻辑编程范例,可应用于非单调推理,叙述式问题求解等领域.本文为ASP提出并实现了一种破圈启发方法与一种基部限制式前向搜索过程,所得到的系统称为LPS.实验结果显示,相对于其他经典的ASP系统,LPS能够有效地解决处于相变难区域中的逻辑程序,通常这些程序被认为是计算困难的.除此以外,通过使用被称为动态变元过滤(dynamic variable filtering,DVF)的技术,LPS可以在计算过程中极大地缩小搜索树的尺寸.     

Consistency argument and classification problem in λ-calculus

Enlightened by Mal'cev theorem in universal algebra, a new criterion for consistency argument in λ-calculus has been introduced. It is equivalent to Jacopini and Baeten-Boerboom' s, but more convenient to use. Based on the new criterion, one uses an enhanced technique to show a few results which provides a deeper insight in the classification problem of λ-terms with no normal forms.     

代数等式系有穷公理化的一个扩充定理

首先介绍两个概念：主同余类的弱可定义性以及次直不可分解类的可定义性.证明了任一有穷代数A,若V(A)具有弱可定义的主同余类以及可定义次直不可分解类,则它的等式系是可以有穷公理化的.进一步的讨论揭示出其结果是新的,是对已有工作的有意义的扩充.     

基于动态时序描述逻辑的动作理论

动态时序描述逻辑(DLTLDL)是一类描述逻辑的动态时序扩展。提出一种基于DLTLALCIO的动态域建模方法,利用该方法可构造出刻画动态域知识的DLTLALCIO理论,并解决动作推理中的框架问题和分支问题。动作推理问题,如动作可执行性和投影问题等,可归结为关于DLTLALCIO理论的推理问题,并最终归结为DLTLALCIO的公式可满足性问题。DLTLALCIO公式可表达动作和时间约束,相对于其他基于描述逻辑的动作形式,基于DLTLALCIO的动作形式在需要执行复杂查询,尤其是含时间或动作的查询的应用场合具有更好的适用性。     

若干限制形式的缺省推理的复杂性

该文研究判定一文字是否出现在缺省理论〈D,W〉的某一扩张中的复杂性.其中,D是一集Horn缺省规则,而W是definite Horn公式或者Bi-Horn公式.     

描述逻辑的动态时序扩展*

在一些基于本体的动态应用中,需要描述组合动作和变化域的时间特性。为了对这类应用建模,通过整合动态时序逻辑和描述逻辑,提出一类描述逻辑扩展。分析了该类扩展的基本形式DLTLALC的语法和语义,并提出一种可终止的tableau算法判别DLTLALC公式可满足性。利用该类扩展,可以表达组合动作执行过程中域变化的时间特性,该类扩展为语义Web服务等动态应用建模和推理提供了一条有效途径。     

Fixed-parameter tractability of disjunction-free default reasoning

In this paper,the parameter which is the source of the complexity of disjunctionfree default reasoning is determined.It is shown that when the value of this parameter is fixed,the disjunction-free default reasoning can be solved time bounded by a polynomial whose degree does not depend on the parameter.Consequently,disjunction-free default reasoning is fixed parameter tractable.     

基于硬件可编程逻辑(FPGA)的SAT算法的综述

可满足性问题(简称SAT问题)作为第一个被证明的NP完全问题,是计算机科学的核心问题之一。本文系统总结了基于硬件可编程逻辑(FPGA---Field Programmable Gate Array)的SAT算法研究。将基于FPGA的SAT算法研究分为了实例型(instance-speci-ed solver)和应用型(application-speci-ed solver)两种类型。通过对各种方法的深入分析,指出了它们的优点和缺陷,进而提出未来研究的思路。