开放的缺省理论

本文基于开放逻辑理论，给出了缺省理论Ｔ＝＜Ｄ，Ｗ＞扩充Ｅ的新假设，事实反驳、ｅ－重构、ｅ－认识进程及其极限等概念的意义，讨论了Ｗ变化时新扩充的变化规律，并证明了相关的定理，本文还建立了缺省理论的一个动态描述过程，证明了其极限是某一特定问题的经验公式集，最后与相关工作进行了比较。     

A Correct Logic Programming Computation of Default Logic Extensions

We present a method of representing some classes of default theories as normal logic programs. The main point is that the standart semantics (i.e., SLDNF-resolution) computes answer substitutions that correspond exactly to the extensions of the represented default theory. This means that we give a correct implementation of default logic. We explain the steps of constructing a logic program LogProg(P, D) from a given default theory (P, D), give some examples, and derive soundness and completeness results.     

Operational concepts of nonmonotonic logics part 1: Default logic

We give an introduction to default logic, one of the most prominent nonmonotonic logics. Emphasis is given to providing an operational interpretation for the semantics of default logic that is usually defined by fixed-point concepts (extensions). We introduce a process model that allows to exactly calculate the extensions of a default theory in a quite easy way. We give a prototypical implementation of processes in Prolog able to handle the examples that can be found in literature. Finally, we develop some theoretical results about default logic and give new simple proofs using the process model as a theoretical tool.     

开放的限制理论

本文基于开放逻辑理论，建立了一阶谓词限制理论的知识增长、更新及理论进化的开放的限制理论，给出了谓词限制理论中新假设、事实反驳及伪事实反驳、Ｃ－重构、Ｃ－认识进程及其极限的定义，讨论了它们的性质并证明了有关的定理，进而描述了限制理论的动态特征－Ｃ－认识进程，证明了其极限定量，并比较了它与一般认识进程及限制理论的关系。     

基于完备拟序的开放逻辑

开放逻辑是一个可以刻画知识的增长，更新以及假说的进化的逻辑理论，它开辟了常识推理研究一条新途径，并在机器学习，知识获取，故障诊断及知识库维护等领域有广泛的应用，基本的开放逻辑不能体现认知主体对所拥有的知识在相信程度上的区别，为此，文中给出了基于完备拟序的开放逻辑，该文采用假说上的完备拟序刻画信度区别，给出了新的重构概念，讨论了假说及完备拟序在知识进化过程中的更新，定义了新的认识进程并证明了所定义的认识进程具有收敛性。     

析取封闭世界假设的一种过程语义

析取信息的表示是一个重要的研究问题.DCWA(析取封闭假设)为一般演绎数据库提供了一种谨慎语义,并且扩充了标准的良基语义.同时DCWA支持争论推理,为广义封闭世界假设提供了一种逼近.基于此,提出了DCWA的过程语义,并证明了它的可靠性和完备性.     

基于四值语义的缺省逻辑

基于公式变换,给出一组缺省理论的变换方法,将命题语言L中的缺省理论变换到对应的命题语言L^-＋中,保证了所得到的缺省理论的所有扩张均不平凡,并通过一种弱变换可同时保证缺省扩张的存在性．为缺省理论定义了各种四值模型,使得缺省逻辑具有非单调超协调推理能力,并证明了L^-＋中的缺省扩张与L中缺省理论的四值模型之间具有一一对应关系．四值模型描述了公式变换的语义,基于四值语义的缺省推理通过缺省理论的变换技术能在标准的缺省逻辑中实现．     

在一类缺省理论中关于证明理论的完备性问题

缺省推理是各种非单调推理系统中最在影响的系统之一。Ｒ。Ｒｅｉｔｅｒ对规范缺省理论作了一系列的研究。他还提出了证明理论，并证明了这一证明理论对于规范缺省理论来说是完备的。Ｗ。Ｅｔｈｅｒｉｎｇｔｏｎ则提出了应用范围更为广泛的有序半规范缺省理论。本文先证明了这类缺省理论具有半单调性等各种性质，然后证明了Ｒ。Ｒｅｉｔｅｒ的证明理论对于有序半规范缺省理论也是完备的。     

An Interpretation of Default Logic in Minimal Temporal Epistemic Logic

When reasoning about complex domains, where information available is usually only partial, nonmonotonic reasoning can be an important tool. One of the formalisms introduced in this area is Reiter's Default Logic (1980). A characteristic of this formalism is that the applicability of default (inference) rules can only be verified in the future of the reasoning process. We describe an interpretation of default logic in temporal epistemic logic which makes this characteristic explicit. It is shown that this interpretation yields a semantics for default logic based on temporal epistemic models. A comparison between the various semantics for default logic will show the differences and similarities of these approaches and ours.     

基于Coq的杨忠道定理形式化证明

实现拓扑学定理的机器证明,是吴文俊院士生前的宿愿.杨忠道定理涉及一般拓扑学中的诸多基本概念,对深刻理解拓扑空间的本质有重要意义.该定理表明,拓扑空间中每一个子集的导集为闭集当且仅当此空间中的每一个单点集的导集为闭集,是一般拓扑学中的一个重要定理.基于定理证明辅助工具Coq,从公理化集合论机器证明系统出发,对一般拓扑学中的开集、闭集、邻域、凝聚点和导集等拓扑基本概念进行形式化描述,给出这些概念基本性质的形式化验证,建立了拓扑空间的形式化框架.在此基础上,实现基于Coq的杨忠道定理形式化证明.全部引理、定理和推论均完整给出Coq的形式化描述和机器证明代码,并在计算机上运行通过,体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点,其证明过程规范、严谨、可靠.杨忠道定理的形式化证明是一般拓扑学形式化内容的一个深刻体现.     

基于模态缺省理论的多Agent系统的知识更新

基于模态缺省理论，建立多Agent系统的模态缺省逻辑，给出了每个主体 对应的模态缺省理论 的新知识和知识冲突的概念及其意义，主要讨论在多Agent环境下，当一个Agent的知识不足以完成推理时，可以从其它Agent处获得新的知识，从而对自身的信念集进行更新。当Wi发生变化(如遇到新的知识或出现与原信念集冲突的知识)时扩充Ei的性质和变化规律，提出了获取新扩充的较简单的求解方法，并证明了相关的定理，给出了多Agent系统的关于知识的一个动态描述过程。     

Analytic fuzzy tableaux

 In this paper Beth–Smullyan's tableaux method is extended to the fuzzy propositional logic. The fuzzy tableaux method is based on the concepts of t-truth and extended graded formula. As in classical logic, it is a refutation procedure. A closed fuzzy tableau beginning with the extended graded formula [r, A] asserting that this is not t-true, is a tableau proof of the graded formula (A, r). The theorems of soundness, completeness, and decidability are proved.     

贪婪缺省逻辑

提出一种贪婪缺省逻辑,旨在构造扩展的过程中尽可能的保留缺省规则当中的信息.给出了贪婪缺省逻辑的推演系统-GD系统和贪婪缺省的GD-扩展的定义.并且证明了对于缺省理论 的一个扩展,必定存在一个贪婪缺省理论的GD-扩展使得缺省逻辑的扩展是贪婪缺省逻辑扩展的子集.并且存在贪婪缺省理论 的某一GD-扩展,该GD-扩展不包含缺省理论的任一扩展.因此缺省逻辑和贪婪缺省逻辑是两种不同的逻辑.     

A Logical Framework for Knowledge Base Maintenance

The maintenance sequences of a knowledge base and their limits are introduced.Some concepts used in knowledge base maintenance,such as new laws,user‘s rejections,and reconstructions of a knowledge base are defined;the related theorems are proved.A procedure is defined using transition systems;it generates maintenance sequences for a given user‘s model and a knowledge base.It is proved that all sequences produced by the procedure are convergent,and their limit is the set of true sentences of the model.Some computational aspects of reconstructions are studied.An R-calculus is given to deduce a reconstruction when a knowledge base meets a user‘s rejection.The work is compared with AGM‘s theory of belief revision.     

Fluid limits and diffusion approximations for networks of multi-server queues in heavy traffic

A Functional Strong-Law-of-Large-Numbers (known as fluid limit or fluid approximation) and a Functional Central Limit Theorem (known as diffusion approximation) are proved for both open and closed networks of multi-server queues in heavy traffic. The fluid limit is a reflected piecewise linear deterministic process, and the diffusion limit is a reflected Brownian motion; both limiting processes are on the nonnegative orthant for open networks and on the nonnegative unit simplex for closed networks. The results generalize the existing ones for networks of single-server queues.     

Consistency properties and set based logic programming

Blair et al. (2001) developed an extension of logic programming called set based logic programming. In the theory of set based logic programming the atoms represent subsets of a fixed universe X and one is allowed to compose the one-step consequence operator with a monotonic idempotent operator O so as to ensure that the analogue of stable models in the theory are always closed under O. Marek et al. (1992, Ann Pure Appl Logic 96:231–276 1999) developed a generalization of Reiter’s normal default theories that can be applied to both default theories and logic programs which is based on an underlying consistency property. In this paper, we show how to extend the normal logic programming paradigm of Marek, Nerode, and Remmel to set based logic programming. We also show how one can obtain a new semantics for set based logic programming based on a consistency property.     

缺省理论与相信理论的关系

本文在相信逻辑中引入相信解释与相信模的概念，从语义上把相信逻辑改造成非单调逻辑。一个缺省理论可以直接转换成一个相信逻辑理论，本文中证明了一个缺省理论外延的模集就是对应相信理论的模，从而为缺省理论提供了一种简便的语义。     

General default logic

In this paper, we propose a new nonmonotonic logic called general default logic. On the one hand, it generalizes Reiter’s default logic by adding to it rule-like operators used in logic programming. On the other hand, it extends logic programming by allowing arbitrary propositional formulas. We show that with this new logic, one can formalize naturally rule constraints, generalized closed world assumptions, and conditional defaults. We show that under a notion of strong equivalence, sentences of this new logic can be converted to a normal form. We also investigate the computational complexity of various reasoning tasks in the logic, and relate it to some other nonmonotonic formalisms such as Lin and Shoham’s logic of GK and Moore’s autoepistemic logic.