Search

We report complexity results about redundancy of formulae in 2CNF form. We first consider the problem of checking redundancy and show some algorithms that are slightly better than the trivial one. We then analyze problems related to finding irredundant equivalent subsets (I.E.S.) of a given set. The concept of cyclicity proved to be relevant to the complexity of these problems. Some results about Horn formulae are also shown., Comment: Corrected figures on Theorem 10; added and modified some references

Temporal Logic Model Checking is a verification method in which we describe a system, the model, and then we verify whether important properties, expressed in a temporal logic formula, hold in the system. Many Model Checking tools employ BDDs or some other data structure to represent sets of states. It has been empirically observed that the BDDs used in these algorithms may grow exponentially as the model and formula increase in size. We formally prove that no kind of data structure of polynomial size can represent the set of valid initial states for all models and all formulae. This result holds for all data structures where a state can be checked in polynomial time. Therefore, it holds not only for all types of BDDs regardless of variable ordering, but also for more powerful data structures, such as RBCs, MTBDDs, ADDs and SDDs. Thus, the size explosion of BDDs is not a limit of these specific data representation structures, but is unavoidable: every formalism used in the same way would lead to an exponential size blow up.

The complexity of deciding equivalence of a formula to an extension of a default theory is investigated for the Reiter, justified, constrained, and rational semantics.

Most of the work in default logic is about default theories that are completely specified. In this category are the proposals of appropriate semantics for default logic, the characterizations of the complexity of reasoning with a default theory, the algorithms for finding consequences of default theories, etc. Relatively little attention has been paid to the process of building a default theory, and most of the work on this topic is about translating knowledge bases from other formalisms (such as circumscription, autoepistemic logic, and action description languages) into default logic. This paper is about expressing knowledge in default logic. In particular, we assume that defaults are initially formulated as normal, and are then corrected using specific inference examples.

This article reports complexity results on diagnosis of systems modeled as graphs. In this model introduced by Rao and Viswanadham, each component is a node of a graph, and an edge indicates that faults propagate from one component to the other one. The basic problem of diagnosis is known to be polynomial and NP-complete in the cases of single faults and multiple faults, respectively. We extend the complexity analysis to the case of faulty alarms, and also consider the problem of limiting the propagation of faults. We show that none of the considered diagnosis problems can be simplified by preprocessing the graph. © 2005 Wiley Periodicals, Inc. Int J Int Syst 20: 1053–1076, 2005.

This article proposes a solution to the problem of obtaining plausibility information, which is necessary to perform belief revision: given a sequence of revisions, together with their results, derive a possible initial order that has generated them; this is different from the usual assumption of starting from an all-equal initial order and modifying it by a sequence of revisions. Four semantics for iterated revision are considered: natural, restrained, lexicographic and reinforcement. For each, a necessary and sufficient condition to the existence of an order generating a given history of revisions and results is proved. Complexity is proved coNP complete in all cases but one (reinforcement revision with unbounded sequence length).

When looking for a propositional abductive explanation of a given set of manifestations, an ordering between possible solutions is often assumed. While the complexity of computing optimal solutions is already known, in this paper we consider second-best solutions with respect to different orderings, and different definitions of what a second-best solution is: an optimal solution not already found, or a solution that is optimal among the ones not previously found.

Some computationally hard problems, e.g., deduction in logical knowledge bases– are such that part of an instance is known well before the rest of it, and remains the same for several subsequent instances of the problem. In these cases, it is useful to preprocess off-line this known part so as to simplify the remaining on-line problem. In this paper we investigate such a technique in the context of intractable, i.e., NP-hard, problems. Recent results in the literature show that not all NP-hard problems behave in the same way: for some of them preprocessing yields polynomial-time on-line simplified problems (we call them compilable), while for other ones their compilability implies some consequences that are considered unlikely. Our primary goal is to provide a sound methodology that can be used to either prove or disprove that a problem is compilable. To this end, we define new models of computation, complexity classes, and reductions. We find complete problems for such classes, “completeness” meaning they are “the less likely to be compilable.” We also investigate preprocessing that does not yield polynomial-time on-line algorithms, but generically “decreases” complexity. This leads us to define “hierarchies of compilability,” that are the analog of the polynomial hierarchy. A detailed comparison of our framework to the idea of “parameterized tractability” shows the differences between the two approaches.

Several methods have been proposed as an attempt to deal with dynamically changing scenarios. From a computational point of view, different formalisms have different computational properties. In this article we consider knowledge bases represented as sets of Horn clauses. The importance of this case is twofold: first, inference is polynomial, thus tractable; second, Horn clauses represents causal relations between facts, thus they are of great practical importance, although not all propositional knowledge bases can be represented in Horn form. The complexity of Horn revision is still high, and in some cases coincides with the complexity of the general (non-Horn) case. We analyze the complexity of belief revision from the point of view of the compilation [Cadoli et al. 1999]: we study the possibility of reducing the complexity by allowing a (possibly expensive) preprocessing of part of the input of the problem. Extending the work of Cadoli et al.[1996], we consider the problem of compact representation of revision in the Horn case, i.e., given a knowledge base T and an update P (both represented by Horn clauses) decide whether T * P , the result of the revision, can be represented with a propositional formula whose size is polynomial in the size of T and P . We give this representation for all formalisms for which it exists, and we show that the existence of a compact representation is related to the possibility of decreasing the complexity of a formalism via a proprocessing.

Belief revision and belief update are two different forms of belief change, and they serve different purposes. In this paper we focus on belief update, the formalization of change in beliefs due to changes in the world. The complexity of the basic update (introduced by Winslett, 1990) has been determined by Eiter and Gottlob (1992). Since then, many other formalizations have been proposed to overcome the limitations and drawbacks of Winslett's update. In this paper we analyze the complexity of the proposals presented in the literature: the standard semantics by Winslett (1986), the minimal change with exception and the minimal change with maximal disjunctive information by Zhang and Foo (1996), the update with disjunctive function by Herzig (1996), the abduction-based update and the generalized update by Boutilier (1996). We relate some of these approaches to belief update to previous work on closed world reasoning.

In this article, we study translations between variants of defaults logics such that the extensions of the theories that are the input and the output of the translation are in a bijective correspondence. We assume that a translation can introduce new variables and that the result of translating a theory can either be produced in time polynomial in the size of the theory or its output is polynomial in that size; we however restrict to the case in which the original theory has extensions. This study fills a gap between two previous pieces of work, one studying bijective translations among restrictions of default logics, and the other one studying non-bijective translations between default logics variants., Removed one useless section

The circumscription of a propositional formula T may not be representable in polynomial space, unless the polynomial hierarchy collapses. This depends on the specific formula T, as some can be circumscribed in little space and others cannot. The problem considered in this article is whether this happens for a given formula or not. In particular, the complexity of deciding whether CIRC(T) is equivalent to a formula of size bounded by k is studied. This theoretical question is relevant as circumscription has applications in temporal logics, diagnosis, default logic and belief revision.

Nonmonotonic formalisms and belief revision operators have been introduced as useful tools to describe and reason about evolving scenarios. Both approaches have been proven effective in a number of different situations. However, little is known about their relationship. Previous work by Winslett has shown some correlations between a specific operator and circumscription. In this paper we greatly extend Winslett's work by establishing new relations between circumscription and a large number of belief revision operators. This highlights similarities and differences between these formalisms. Furthermore, these connections provide us with the possibility of importing results in one field into the other one.

Many variants of default logics exist. Two of the main differences among them arise from the choice between local and global consistency, and the choice of whether or not to accept maximally successful sets of defaults. In this paper, we characterize theories that do not depend at all on what makes the semantics different, that is, theories for which these two choices do not matter. A result that is proved for such theories holds not only for all the considered semantics, but also for every other semantics that differs from them on the two choices.

In this paper we address a specific computational aspect of belief revision: the size of the propositional formula obtained by means of the revision of a formula with a new one. In particular, we focus on the size of the smallest formula which is logically equivalent to the revised knowledge base. The main result of this paper is that not all formalizations of belief revision are equal from this point of view. For some of them we show that the revised knowledge base can be represented by a polynomial-size formula (we call these results “compactability” results). On the other hand, for other ones the revised knowledge base does not always admit a polynomial-space representation, unless the polynomial hierarchy collapses at a sufficiently low level (“non-compactability” results). We also show that the time complexity of query answering for the revised knowledge base has definitely an impact on being able to represent the result of the revision compactly. Nevertheless, formalisms with the same complexity may have different compactability properties. We also study compactability properties for a weaker form of equivalence, called query equivalence, which allows to introduce new propositional symbols. Moreover, we extend our analysis to the special case in which the new formula has constant size and to the case of sequences of revisions (i.e., iterated belief revision). A complete analysis along these four coordinates is shown. ∗An extended abstract of this paper appeared as [5]. †Current address: Politecnico di Bari, Dipartimento di Elettrotecnica ed Elettronica, Via E. Orabona 4, I-70125 Bari, Italy.

In this paper we analyze the complexity of revising a knowledge base when an iteration of this process is necessary. The analysis concerns both the classical problems of belief revision (inference, model checking, computation of the new base) and new issues, related to the problem of “committing” the changes.

A knowledge base is redundant if it contains parts that can be inferred from the rest of it. We study the problem of checking whether a CNF formula (a set of clauses) is redundant, that is, it contains clauses that can be derived from the other ones. Any CNF formula can be made irredundant by deleting some of its clauses: what results is an irredundant equivalent subset (I.E.S.) We study the complexity of some related problems: verification, checking existence of a I.E.S. with a given size, checking necessary and possible presence of clauses in I.E.S.'s, and uniqueness. We also consider the problem of redundancy with different definitions of equivalence., Comment: Extended and revised version of a paper that has been presented at ECAI 2002

Independence—the study of what is relevant to a given problem of reasoning—is an important AI topic. In this paper, we investigate several notions of conditional independence in propositional logic: Darwiche and Pearl's conditional independence, and some more restricted forms of it. Many characterizations and properties of these independence relations are provided. We show them related to many other notions of independence pointed out so far in the literature (mainly formula-variable independence, irrelevance and novelty under various forms, separability, interactivity). We identify the computational complexity of conditional independence and of all these related independence relations.

One of the main challenges in the formal modeling of common-sense reasoning is the ability to cope with the dynamic nature of the world. Among the approaches put forward to address this problem are belief revision and update. Given a knowledge base T, representing our knowledge of the “state of affairs” of the world of interest, it is possible that we are led to trust another piece of information P, possibly inconsistent with the old one T. The aim of revision and update operators is to characterize the revised knowledge base T′ that incorporates the new formula P into the old one T while preserving consistency and, at the same time, avoiding the loss of too much information. In this paper we study the computational complexity, in the propositional case, of one of the main reasoning problems of belief revision and update: deciding if an interpretation M is a model of the revised knowledge base.