We present an approach to database update as a form of non monotonic temporal reasoning, the main idea of which is the (circumscriptive) minimization of changes with respect to a set of facts declared “persistent by default”. The focus of the paper is on the relation between this approach and the update semantics recently proposed by Katsuno and Mendelzon. Our contribution in this regard is twofold:We prove a representation theorem for KM semantics in terms of a restricted subfamily of the (...) operators defined by our construction.We show how the KM semantics can be generalized by relaxing our construction in a number of ways, each justified in certain intuitive circumstances and each corresponding to one specific postulate. It follows that there are reasonable update operators outside the KM family.Our approach is not dependent for its plausibility on this connection with KM semantics. Rather, it provides a relatively rich and flexible framework in which the frame and ramification problems can be solved in a systematic way by reasoning about default persistence of facts. (shrink)

Based on a close study of benchmark examples in default reasoning, such as Nixon Diamond, Penguin Principle, etc., this paper provides an in depth analysis of the basic features of default reasoning. We formalize default inferences based on Modus Ponens for Default Implication, and mark the distinction between "local inferences"(to infer a conclusion from a subset of given premises) and "global inferences"(to infer a conclusion from the entire set of given premises). These conceptual analyses are captured by a formal semantics (...) that is built upon the set-selection function technique. A minimal logic system M of default reasoning that accommodates Modus Ponens for Default Implication and suitable for local inferences is proposed, and its soundness is proved. (shrink)

In the current paper we consider theories with vocabulary containing a number of binary and unary relation symbols. Binary relation symbols represent labeled edges of a graph and unary relations represent unique annotations of the graph's nodes. Such theories, which we call annotation theories^ can be used in many applications, including the formalization of argumentation, approximate reasoning, semantics of logic programs, graph coloring, etc. We address a number of problems related to annotation theories over finite models, including satisfiability, querying problem, (...) specification of preferred models and model checking problem. We show that most of considered problems are NPTime- or co-NPTime-complete. In order to reduce the complexity for particular theories, we use second-order quantifier elimination. To our best knowledge none of existing methods works in the case of annotation theories. We then provide a new second-order quantifier elimination method for stratified theories, which is successful in the considered cases. The new result subsumes many other results, including those of [2, 28, 21]. (shrink)