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. (shrink)

In recent years much effort has gone into the study of languages which strengthen the classical first-order predicate calculus in various ways. This effort has been motivated by the desire to find a language which is(I) strong enough to express interesting properties not expressible by the classical language, but(II) still simple enough to yield interesting general results. Languages investigated include second-order logic, weak second-order logic, ω-logic, languages with generalized quantifiers, and infinitary logic.

In this article, we compare the expressive powers of classes of normal logic programs that are obtained by constraining the number of positive subgoals in the bodies of rules. The comparison is based on the existence/nonexistence of polynomial, faithful, and modular translation functions between the classes. As a result, we obtain a strict ordering among the classes under consideration. Binary programs are shown to be as expressive as unconstrained programs but strictly more expressive than unary programs which, in turn, are (...) strictly more expressive than atomic programs. We also take propositional theories into consideration and prove them to be strictly less expressive than atomic programs. In spite of the gap in expressiveness, we develop a faithful but non-modular translation function from normal programs to propositional theories. We consider this as a breakthrough due to sub-quadratic time complexity |). Furthermore, we present a prototype implementation of the translation function and demonstrate its promising performance with SAT solvers using three benchmark problems. (shrink)