We study uniform interpolation and forgetting in the description logic ALC. Our main results are model-theoretic characterizations of uniform interpolants and their existence in terms of bisimulations, tight complexity bounds for deciding the existence of uniform interpolants, an approach to computing interpolants when they exist, and tight bounds on their size. We use a mix of model-theoretic and automata-theoretic methods that, as a by-product, also provides charachterizations of, and decision procedures for, conservative extensions.

In a seminal paper, Lin and Reiter introduced the notion of progression for basic action theories in the situation calculus. Earlier works by Moore, Scherl and Levesque extended the situation calculus to account for knowledge. In this paper, we study progression of knowledge in the situation calculus. We first adapt the concept of bisimulation from modal logic and extend Lin and Reiter's notion of progression to accommodate knowledge. We show that for physical actions, progression of knowledge reduces to forgetting predicates in first-order modal logic. We identify a class of first-order modal formulas for which forgetting an atom is definable in first-order modal logic. This class of formulas goes beyond formulas without quantifying-in. We also identify a simple case where forgetting a predicate reduces to forgetting a finite number of atoms. Thus we are able to show that for local-effect physical actions, when the initial KB is a formula in this class, progression of knowledge is definable in first-order modal logic. Finally, we extend our results to the multi-agent case.

Since the seminal work of Sampath et al. in 1996, despite the subsequent flourishing of techniques on diagnosis of discrete-event systems (DESs), the basic notions of fault and diagnosis have been remaining conceptually unchanged. Faults are defined at component level and diagnoses incorporate the occurrences of component faults within system evolutions: diagnosis is context-free. As this approach may be unsatisfactory for a complex DES, whose topology is organized in a hierarchy of abstractions, we propose to define different diagnosis rules for different subsystems in the hierarchy. Relevant fault patterns are specified as regular expressions on patterns of lower-level subsystems. Separation of concerns is achieved and the expressive power of diagnosis is enhanced: each subsystem has its proper set of diagnosis rules, which may or may not depend on the rules of other subsystems. Diagnosis is no longer anchored to components: it becomes context-sensitive. The approach yields seemingly contradictory but nonetheless possible scenarios: a subsystem can be normal despite the faulty behavior of a number of its components (positive paradox); also, it can be faulty despite the normal behavior of all its components (negative paradox).

Existential rules, i.e. Datalog extended with existential quantifiers in rule heads, are currently studied under a variety of names such as Datalog +/-, ∀∃-rules, and tuple-generating dependencies. The renewed interest in this formalism is fuelled by a wealth of recently discovered language fragments for which query answering is decidable. This paper extends and consolidates two of the main approaches in this field — acyclicity and guardedness — by providing (1) complexity-preserving generalisations of weakly acyclic and weakly (frontier-)guarded rules, and (2) a novel formalism of glut-(frontier-)guarded rules that subsumes both. This builds on an insight that acyclicity can be used to extend any existential rule language while retaining decidability. Besides decidability, combined query complexities are established in all cases.

We investigate (quantifier-free) spatial constraint languages with equality, contact and connectedness predicates as well as Boolean operations on regions, interpreted over low-dimensional Euclidean spaces. We show that the complexity of reasoning varies dramatically depending on the dimension of the space and on the type of regions considered. For example, the logic with the interior-connectedness predicate (and without contact) is undecidable over polygons or regular closed sets in the Euclidean plane, NP-complete over regular closed sets in three-dimensional Euclidean space, and ExpTime-complete over polyhedra in three-dimensional Euclidean space.

Existing belief merging operators take advantage of all the models from the bases, including those contradicting the integrity constraints. In this paper, we show that this is not suited to every merging scenario. We study the case when the bases are "rationalized" with respect to the integrity constraints during the merging process. We define in formal terms several independence conditions for merging operators and show how they interact with the standard IC postulates for belief merging. Especially, we give an independence-based axiomatic characterization of a distance-based operator.

Many applications of causal inference, such as finding the relationship between stock prices and news reports, involve both discrete and continuous variables observed over time. Inference with these complex sets of temporal data, though, has remained difficult and required a number of simplifications. We show that recent approaches for inferring temporal relationships (represented as logical formulas) can be adapted for inference with continuous valued effects. Building on advances in logic, PCTLc (an extension of PCTL with numerical constraints) is introduced here to allow representation and inference of relationships with a mixture of discrete and continuous components. Then, finding significant relationships in the continuous case can be done using the conditional expectation of an effect, rather than its conditional probability. We evaluate this approach on both synthetically generated and actual financial market data, demonstrating that it can allow us to answer different questions than the discrete approach can.

Recent years have seen a lot of work towards extending the established AGM belief revision theory with respect to iterating revision, preserving conditional beliefs, and handling sets of propositions as new information. In particular, novel postulates like independence and evidence retainment have been brought forth as new standards for revising epistemic states by (sets of) propositional information. In this paper, we propose a constructive approach for revising epistemic states by sets of (propositional and conditional) beliefs that combines ideas from nonmonotonic reasoning with conditional belief revision. We also propose a novel principle called enforcement that covers both independence and evidence retainment, and we show our revision operator to comply with major postulates from the literature. Moreover, we point out the relevance of our approach for default reasoning.

Temporal reasoning problems arise in many areas of AI, including planning, natural language understanding, and reasoning about physical systems. The computational complexity of continuous-time temporal constraint reasoning is fairly well understood. There are, however, many different cases where discrete time must be considered; various scheduling problems and reasoning about sampled physical systems are two examples. Here, the complexity of temporal reasoning is not as well-studied nor as well-understood. In order to get a better understanding, we consider the powerful Horn DLR formalism adapted for discrete time and study its computational complexity. We show that the full formalism is NP-hard and identify several maximal tractable subclasses. We also ‘lift’ the maximality results to obtain hardness results for other families of constraints. Finally, we discuss how the results and techniques presented in this paper can be used for studying even more expressive classes of temporal constraints.

The Boolean network is a mathematical model of biological systems, and has attracted much attention as a qualitative tool for analyzing the regulatory system. The stable states and dynamics of Boolean networks are characterized by their attractors, whose properties have been analyzed computationally, yet not much work has been done from the viewpoint of logical inference systems. In this paper, we show direct translations of Boolean networks into logic programs, and propose new methods to compute their trajectories and attractors based on inference on such logic programs. In particular, point attractors of both synchronous and asynchronous Boolean networks are characterized as supported models of logic programs so that SAT techniques can be applied to compute them. Investigation of these relationships suggests us to view Boolean networks as logic programs and vice versa.