Possibilistic logic is a well-known logic for reasoning under uncertainty, which is based on the idea that the epistemic state of an agent can be modeled by assigning to each possible world a degree of possibility, taken from a totally ordered, but essentially qualitative scale. Recently, a generalization has been proposed that extends possibilistic logic to a meta-epistemic logic, endowing it with the capability of reasoning about epistemic states, rather than merely constraining them. In this paper, we further develop this generalized possibilistic logic (GPL). We introduce an axiomatization showing that GPL is a fragment of a graded version of the modal logic KD, and we prove soundness and completeness w.r.t. a semantics in terms of possibility distributions. Next, we reveal a close link between the well-known stable model semantics for logic programming and the notion of minimally specific models in GPL. More generally, we analyze the relationship between the equilibrium logic of Pearce and GPL, showing that GPL can essentially be seen as a generalization of equilibrium logic, although its notion of minimal specificity is slightly more demanding than the notion of minimality underlying equilibrium logic.

A constraint satisfaction problem has compactness if any infinite set of constraints is satisfiable whenever all its finite subsets are satisfiable. We prove a sufficient condition for compactness, which holds for a range of problems including those based on the well-known Interval Algebra (IA) and RCC8. Furthermore, we show that compactness leads to a useful necessary and sufficient condition for the recently introduced patchwork property, namely that patchwork holds exactly when every satisfiable finite network (i.e., set of constraints) has a canonical solution, that is, a solution that can be extended to a solution for any satisfiable finite extension of the network. Applying these general theorems to qualitative reasoning, we obtain important new results as well as significant strengthenings of previous results regarding IA, RCC8, and their fragments and extensions. In particular, we show that all the maximal tractable fragments of IA and RCC8 (containing the base relations) have patchwork and canonical solutions as long as networks are algebraically closed.

We present a conflict-based approach to diagnosing Discrete Event Systems (DES) which generalises Reiter's Diagnose algorithm to a much broader class of problems. This approach obviates the need to explicitly reconstruct the system's behaviors that are consistent with the observation, as is typical of existing DES diagnosis algorithms. Instead, our algorithm explores the space of diagnosis hypotheses, testing hypotheses for consistency, and generating conflicts which rule out successors and other portions of the search space. Under relatively mild assumptions, our algorithm correctly computes the set of preferred diagnosis candidates. We investigate efficient symbolic representations of the hypotheses space and provide a SAT-based implementation of this framework which is used to address a real-world problem in processing alarms for a power transmission system.

We consider the problem of synthesizing an agent pro- tocol satisfying LTL specifications for multiple, partially- observable environments. We present a sound and complete procedure for solving the synthesis problem in this setting and show it is computationally optimal from a theoretical com- plexity standpoint. While this produces perfect-recall, hence unbounded, strategies we show how to transform these into agent protocols with bounded number of states.

Abstraction has been used in search and planning from the very beginning of AI. Many different methods and formalisms for abstraction have been proposed in the literature but they have been designed from various points of view and with varying purposes. Hence, these methods have been notoriously difficult to analyse and compare in a structured way. In order to improve upon this situation, we present a coherent and flexible framework for modelling abstraction (and abstraction-like) methods based on transformations on labelled graphs. Transformations can have certain method properties that are inherent in the abstraction methods and describe their fundamental modelling characteristics, and they can have certain instance properties that describe algorithmic and computational characteristics of problem instances. The usefulness of the framework is demonstrated by applying it to problems in both search and planning. First, we show that we can capture many search abstraction concepts (such as avoidance of backtracking between levels) and that we can put them into a broader context. We further model five different abstraction concepts from the planning literature. Analysing what method properties they have highlights their fundamental differences and similarities. Finally, we prove that method properties sometimes imply instance properties. Taking also those instance properties into account reveals important information about computational aspects of the five methods.

We define generalized ontology-based production systems (GOPSs), which formalize a very general and powerful combination of ontologies and production systems. We show that GOPSs capture and generalize many existing formal notions of production systems. We introduce a powerful verification query language for GOPSs, which is able to express the most relevant formal properties of production systems previously considered in the literature. We establish a general sufficient condition for the decidability of answering verification queries over GOPSs. Then, we define Lite-GOPS, a particular class of GOPSs based on the use of a light-weight ontology language (DL-Llite_A), a light-weight ontology query language (EQL-Lite(UCQ)), and a tractable semantics for updates over Description Logic ontologies. We show decidability of all the above verification tasks over Lite-GOPSs, and prove tractability of some of such tasks.

A large and complex knowledge base that models some aspect of the real world can rarely be fully specified. Two examples of such underspecification are that (i) some of the cardinality constraints are omitted; (ii) some properties of all individual instances of a class are specialized across a class hierarchy, but specific references to which particular values are specialized are omitted. Such knowledge bases are of great practical interest as they are the basis of an empirically tested knowledge acquisition system that has been used to construct a knowledge base from a significant portion of a biology textbook. In this paper, we formalize an underspecified knowledge base using answer set programming, and give a set of rules called UMAP that support inheritance reasoning in such a knowledge base.

In this paper we encode some of the reasoning methods used in frame based knowledge representation languages in answer set programming (ASP). In particular, we show how ``cloning'' and ``unification'' in frame based systems can be encoded in ASP. We then show how some of the types of queries with respect to a biological knowledge base can be encoded using our methodology. We also provide insight on how the reasoning can be done more efficiently when dealing with a huge knowledge base.

Given a 4-tuple of Boolean variables (a, b, c, d), logical proportions are modeled by a pair of equivalences relating similarity indicators (a ∧ b and a ∧ b), or dissimilarity indicators (a ∧ b and a ∧ b) pertaining to the pair (a, b), to the ones associated with the pair (c, d). Logical proportions are homogeneous when they are based on equivalences between indicators of the same kind. There are only 4 such homogeneous proportions, which respectively express that i) “a differs from b as c differs from d” (and “b differs from a as d differs from c”), ii) “a differs from b as d differs from c” (and “b differs from a as c differs from d”), iii) “what a and b have in common c and d have it also”, iv) “what a and b have in common neither c nor d have it”. We prove that each of these proportions is the unique Boolean formula (up to equivalence) that satisfies groups of remarkable properties including a stability property w.r.t. a specific permutation of the terms of the proportion. The first one (i) is shown to be the only one to satisfy the standard postulates of an analogical proportion. The paper also studies how two analogical proportions can be combined into a new one. We then examine how homogeneous proportions can be used for diverse prediction tasks. We particularly focus on the completion of analogical-like series, and on missing value abduction problems. Finally, the paper compares our approach with other existing works on qualitative prediction based on ideas of betweenness, or of matrix abduction.

We consider the problem of reasoning from inconsistent hybrid theories, i.e., combinations of a structural part given by a classical first order theory (e.g., an ontology) and a rules part as a set of declarative logic program rules (under answer-set semantics). Paraconsistent reasoning is achieved by defining an appropriate semantics, so-called paraconsistent semi-equilibrium model semantics for such hybrid theories. Appropriateness of the semantics is established with respect to desirable properties attesting design objectives, such us to generalize the underlying semantics in case of consistency, as well as to generalize existing paraconsistent semantics for the individual parts. A complexity analysis of corresponding reasoning tasks complements these results.