On embedding default logic into Moore''s autoepistemic logic

Recently Gottlob proved [2] that there does not exist a faithful modular translation of default logic into autoepistemic logic, and presented a non-modular translation. Gottlob's translation, however, is indirect (it uses “nonmonotonic logic N” as an intermediate point), quite complex and exploits sophisticated encoding of proof theory in autoepistemic formulas. We provide a simpler and more intuitive (non-modular) direct translation. In addition, our argument is purely model-theoretic.     

Uniform semantic treatment of default and autoepistemic logics

We revisit the issue of epistemological and semantic foundations for autoepistemic and default logics, two leading formalisms in nonmonotonic reasoning. We develop a general semantic approach to autoepistemic and default logics that is based on the notion of a belief pair and that exploits the lattice structure of the collection of all belief pairs. For each logic, we introduce a monotone operator on the lattice of belief pairs. We then show that a whole family of semantics can be defined in a systematic and principled way in terms of fixpoints of this operator (or as fixpoints of certain closely related operators). Our approach elucidates fundamental constructive principles in which agents form their belief sets, and leads to approximation semantics for autoepistemic and default logics. It also allows us to establish a precise one-to-one correspondence between the family of semantics for default logic and the family of semantics for autoepistemic logic. The correspondence exploits the modal interpretation of a default proposed by Konolige. Our results establish conclusively that default logic can be viewed as a fragment of autoepistemic logic, a result that has been long anticipated. At the same time, they explain the source of the difficulty to formally relate the semantics of default extensions by Reiter and autoepistemic expansions by Moore. These two semantics occupy different locations in the corresponding families of semantics for default and autoepistemic logics.     

Modal nonmonotonic logics demodalized

The study of the relation between default logic and modal nonmonotonic logics has been mostly concerned with the task of translating default logic to autoepistemic or some other modal nonmonotonic logic. Here, we discuss the reverse problem, that is, the possibility of translating modal nonmonotonic logics into default-type systems formulated in the language without modal operators. To this end, we first consider a reformulation of both formalisms in terms of what we call default consequence relations. These consequence relations turn out to be especially suitable for studying default and modal nonmonotonic reasoning. We show, in particular, that different kinds of such reasoning naturally correspond to different structural rules imposed on default consequence relations. Our main results also demonstrate that all modal nonmonotonic objects considered have exact nonmodal counterparts. As an immediate consequence of these results, we obtain a method of reducing common types of modal nonmonotonic reasoning to nonmodal default reasoning.     

Autoepistemic logic of first order and its expressive power

We study the expressive power of first-order autoepistemic logic. We argue that full introspection of rational agents should be carried out by minimizing positive introspection and maximizing negative introspection. Based on full introspection, we propose the maximal well-founded semantics that characterizes autoepistemic reasoning processes of rational agents, and show that breadth of the semantics covers all theories in autoepistemic logic of first order, Moore's AE logic, and Reiter's default logic. Our study demonstrates that the autoepistemic logic of first order is a very powerful framework for nonmonotonic reasoning, logic programming, deductive databases, and knowledge representation.This research is partially supported by NSERC grant OGP42193.     

基于四值语义的缺省逻辑

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

Strong and uniform equivalence of nonmonotonic theories – an algebraic approach

We show that the concepts of strong and uniform equivalence of logic programs can be generalized to an abstract algebraic setting of operators on complete lattices. Our results imply characterizations of strong and uniform equivalence for several nonmonotonic logics including logic programming with aggregates, default logic and a version of autoepistemic logic. This work was partially supported by the NSF grant IIS-0325063.     

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.     

Reasoning with Sets of Defaults in Default Logic

We present a general approach for representing and reasoning with sets of defaults in default logic, focusing on reasoning about preferences among sets of defaults. First, we consider how to control the application of a set of defaults so that either all apply (if possible) or none do (if not). From this, an approach to dealing with preferences among sets of default rules is developed. We begin with an ordered default theory , consisting of a standard default theory, but with possible preferences on sets of rules. This theory is transformed into a second, standard default theory wherein the preferences are respected. The approach differs from other work, in that we obtain standard default theories and do not rely on prioritized versions of default logic. In practical terms this means we can immediately use existing default logic theorem provers for an implementation. Also, we directly generate just those extensions containing the most preferred applied rules; in contrast, most previous approaches generate all extensions, then select the most preferred. In a major application of the approach, we show how semimonotonic default theories can be encoded so that reasoning can be carried out at the object level. With this, we can reason about default extensions from within the framework of a standard default logic. Hence one can encode notions such as skeptical and credulous conclusions, and can reason about such conclusions within a single extension.     

A Critical Reexamination of Default Logic, Autoepistemic Logic, and Only Knowing

Fifteen years of work on nonmonotonic logic has certainly increased our understanding of the area. However, given a problem in which nonmonotonic reasoning is called for, it is far from clear how one should go about modeling the problem using the various approaches. We explore this issue in the context on two of the best–known approaches, Reiter's default logic and Moore's autoepistemic logic, as well as two related notions of "only knowing," due to Halpern and Moses and to Levesque. In particular, we return to the original technical definitions given in these papers and examine the extent to which they capture the intuitions they were designed to capture.     

Default logic as a query language

Research in nonmonotonic reasoning has focused largely on the idea of representing knowledge about the world via rules that are generally true but can be defeated. Even if relational databases are nowadays the main tool for storing very large sets of data, the approach of using nonmonotonic AI formalisms as relational database query languages has been investigated to a much smaller extent. In this work, we propose a novel application of Reiter's default logic by introducing a default query language (DQL) for finite relational databases, which is based on default rules. The main result of this paper is that DQL is as expressive as SO_∃∀ the existential-universal fragment of second-order logic. This result is not only of theoretical importance: We exhibit queries-which are useful in practice-that can be expressed with DQL and cannot with other query languages based on nonmonotonic logics such as DATALOG with negation under the stable model semantics. In particular, we show that DQL is well-suited for diagnostic reasoning     

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

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

Nonmonotonic consequences in default domain theory

Default domain theory is a framework for representing and reasoning about commonsense knowledge. Although this theory is motivated by ideas in Reiter’s work on default logic, it is in some sense a dual framework. We make Reiter’s default extension operator into a constructive method of building models, not theories. Domain theory, which is a well established tool for representing partial information in the semantics of programming languages, is adopted as the basis for constructing partial models. This paper considers some of the laws of nonmonotonic consequence, due to Gabbay and to Kraus, Lehmann, and Magidor, in the light of default domain theory. We remark that in some cases Gabbay’s law of cautious monotony is open to question. We consider an axiomatization of the nonmonotonic consequence relation on prime open sets in the Scott topology – the natural logic – of a domain, which omits this law. We prove a representation theorem showing that such relations are in one to one correspondence with the consequence relations determined by extensions in Scott domains augmented with default sets. This means that defaults are very expressive: they can, in a sense, represent any reasonable nonmonotonic entailment. Results about what kind of defaults determine cautious monotony are also discussed. In particular, we show that the property of unique extensions guarantees cautious monotony, and we give several classes of default structures which determine unique extensions. This revised version was published online in June 2006 with corrections to the Cover Date.