ABSTRACT. Ontologies based on Description Logics may contain errors, which are usually detected when reasoning produces consequencesthat follow from the ontology, but do not hold in the modelled application domain. In previous work, we have introducedrepair approaches for  \EL ontologies that are optimal in the sense that they preserve a maximal amount of consequences.  In this paper, we will, on the one hand, review these approaches, but with an emphasis on motivation rather than on technical details. On the other hand, we will describe new results that address the problems that optimal repairs may become very large or need not even exist unless strong restrictions on the terminological part of the ontology apply.We will show how one can deal with these problems by introducing concise representations of optimal repairs.

ABSTRACT. Modal logics are widely used in multi-agent systems to rea- son about actions, abilities, norms, or epistemic states. Combined with description logic languages, they are also a powerful tool to formalise modal aspects of ontology-based reasoning over an object domain. However, the standard relational semantics for modalities is known to validate principles deemed problematic in agency, deontic, or epistemic applications. To overcome these difficulties, weaker systems of so-called non-normal modal logics, equipped with neighbourhood semantics that generalise the relational one, have been investigated both at the propositional and at the description logic level. We present here a family of non-normal modal description logics, obtained by extending ALC-based languages with non-normal modal operators. For formulas interpreted on neighbourhood models over varying domains, we provide a modular framework of terminating, correct, and complete tableau-based satisfiability checking algorithms in NExpTime. For a subset of these systems, we also consider a reduction to satisfiability on constant domain relational models. Moreover, we investigate the satisfiability problem in fragments obtained by disallowing the application of modal operators to description logic concepts, providing tight ExpTime complexity results.

ABSTRACT. This paper establishes alternative characterizations of very expressive classes of existential rule sets with decidable query entailment. We consider the notable class of greedy bounded-treewidth sets (gbts) and a new, generalized variant, called weakly gbts (wgbts). Revisiting and building on the notion of derivation graphs, we define (weakly) cycle-free derivation graph sets ((w)cdgs) and employ elaborate proof-theoretic arguments to obtain that gbts and cdgs coincide, as do wgbts and wcdgs. These novel characterizations advance our analytic proof-theoretic understanding of existential rules and will likely be instrumental in practice.

ABSTRACT. We consider the problem of optimal planning in deterministic domains specified with expressive action languages. We show how it is possible to reduce such problem to the one of finding an optimal solution of a constraint optimization problem incorporating a bound $n$ on the maximum length of the plan. By solving the latter, we can conclude whether $(i)$ the plan found is optimal even for bounds greater than $n$; or $(ii)$ we need to increase $n$; or $(iii)$ it is useless to increase $n$ since the planning problem has no solution. Our approach $(i)$ substantially generalizes previous approaches for optimal symbolic deterministic planning; $(ii)$ enables us to compute non trivial lower bounds on the cost and length of optimal plans; and $(iii)$ produces an encoding linear in the size of the planning problem and the bound $n$.

ABSTRACT. Geffner & Geffner (2018) have shown that finding plans by reduction to SAT is not limited to classical planning, but is competitive also for fully observable non-deterministic planning. This work extends these ideas to planning with partial observability. Specifically, we handle partial observability by requiring that during the execution of a plan, the same actions have to be taken in all indistinguishable circumstances. We demonstrate that encoding this condition directly leads to far better scalability than an explicit encoding of observations-to-actions mapping, for high numbers of observations.

ABSTRACT. Dynamic Epistemic Logic (DEL) provides a framework for epistemic planning that is capable of representing non-deterministic actions, partial observability, higher-order knowledge and both factual and epistemic change. The high expressivity of DEL challenges existing epistemic planners, which typically can handle only restricted fragments of the whole framework. The goal of this work is to push the envelop of practical DEL planning, ultimately aiming for epistemic planners to be able to deal with the full range of features offered by DEL. Towards this goal, we question the traditional semantics of DEL, defined in terms on Kripke models. In particular, we propose an equivalent semantics defined using, as main building block, so-called possibilities: non well-founded objects representing both factual properties of the world, and what agents consider to be possible. We call the resulting framework DELPHIC. We argue that DELPHIC indeed provides a more compact representation of epistemic states. To substantiate this claim, we implement both approaches in ASP and we set up an experimental evaluation to compare DELPHIC with the traditional, Kripke-based approach. The evaluation confirms that DELPHIC outperforms the traditional approach in space and time.

ABSTRACT. This paper proposes a framework for representing and reasoning about the plan selection process of an autonomous agent that is expected to operate within the boundaries of a given policy. We assume that the agent takes into consideration both policy compliance and plan length, and may prioritize one of these aspects over the other, based on circumstances. We consider authorization and obligation policies specified in the language AOPL by Gelfond and Lobo. Our framework builds upon the AAA agent architecture and is implemented in ASP.

ABSTRACT. Temporal planning is an extension of classical planning involving concurrent execution of actions and alignment with temporal constraints. Unfortunately, the performance of temporal planning engines tends to sharply deteriorate when the number of agents and objects in a domain gets large. A possible remedy is to use macro-actions that are well-studied in the context of classical planning. In temporal planning settings, however, introducing macro-actions is significantly more challenging when the concurrent execution of actions and shared use of resources, provided the compliance to temporal constraints, should not be suppressed entirely. Our work contributes a general concept of sequential temporal macro-actions that guarantees the applicability of obtained plans, i.e., the sequence of original actions encapsulated by a macro-action is always executable. We apply our approach to several temporal planners and domains, stemming from the International Planning Competition and RoboCup Logistics League. Our experiments yield improvements in terms of obtained satisficing plans as well as plan quality for the majority of tested planners and domains.

ABSTRACT. In multi-agent system design, a crucial aspect is to ensure robustness, meaning that for a coalition of agents A, small violations of adversarial assumptions only lead to small violations of A's goals. In this paper we introduce a logical framework for robust strategic reasoning about multi-agent systems. Specifically, inspired by recent works on robust temporal logics, we introduce and study rATL and rATL*, logics that extend the well-known Alternating-time Temporal Logic ATL and ATL* by means of an opportune multi-valued semantics for the strategy quantifiers and temporal operators. We study the model-checking and satisfiability problems for rATL and rATL* and show that dealing with robustness comes at no additional computational cost. Indeed, we show that these problems are PTIME-complete and EXPTIME-complete for rATL, respectively, while both are 2EXPTIME-complete for rATL*.

ABSTRACT. Extensions of Answer Set Programming with language constructs from temporal logics, such as temporal equilibrium logic over finite traces (TELf), provide an expressive computational framework for modeling dynamic applications.

In this paper, we study the so-called past-present syntactic subclass, which consists of a set of logic programming rules whose body references to the past and its head to the present. Such restriction ensures that the past remains independent of the future, which is the case in most dynamic domains.

We extend the definition of completion and loop formulas to the case of past-present formulas, which allows capturing the TELf models of a set past-present formulas by means of an LTLf expression.

ABSTRACT. Building on previous work on Weighted Description Logic (WDL), we present and assess an algorithm for concept combination grounded in the experimental research in cognitive psychology. Starting from two WDL formulas (representing concepts in a way similar to Prototype Theory) and a knowledge base (KB) modelling background knowledge, the algorithm outputs a new WDL formula which represent the combination of the input concepts. First, we study the logical properties of the operator defined by our algorithm. Second, we collect data on the prototypical representation of concepts and their combinations and learn WDL formulas from them. Third, we evaluate our algorithm and the role of the KB by comparing the algorithm's outputs with the learned WDL formulas.

ABSTRACT. Minimal Hitting Set (MHS) is a well-known and complete method to compute all explanations of an ABox abduction problem in Description Logics (DL). MHS is NP-complete and generally recognized as inefficient. MergeXplain (MXP), on the other hand, is fast but does not guarantee to find all explanations. We present MHS-MXP, a hybrid algorithm which adopts the divide-and-conquer strategy of MXP and combines it with MHS to regain completeness. In this paper, we describe: (a) the underlying theory to establish the completeness of MHS-MXP and show its relevant properties; (b) a class of inputs on which MHS-MXP has the greatest advantage; (c) an experimental implementation based on true black-box integration with the JFact reasoner; (d) an empirical evaluation on two classes of inputs (one unfavourable and one favourable).

ABSTRACT. This paper falls within the context of Ontology-Based Data Access and deals with inconsistent partially ordered lightweight ontologies. It introduces a new method for computing data repairs and shows that it is tractable in the possibilistic setting, where uncertainty concerns only the data elements. The proposed method is called Cπ-repair and computes a single data repair, in the spirit of the Intersection of ABox Repair (IAR) semantics, as follows. It first interprets the partially ordered dataset as a family of totally ordered datasets. Then, it computes a single data repair for every totally ordered possibilistic ontology induced from the partially ordered possibilistic ontology. Next, it deductively closes each of these repairs in order to increase their productivity in a safe way (since they are conflict-free). Finally, it intersects the closed repairs to obtain a single data repair for the initial ontology. The main contribution of this paper is an equivalent characterization that does not enumerate all the total orders and also does not suffer from the additional computational cost naturally incurred by the deductive closure. We establish the tractability of our method by reformulating the problem using the notions of dominance and support. Intuitively, the Cπ-repair method returns only the elements that are supported against conflicts by consistent inclusion-minimal subsets that dominate all the conflicts within the dataset. We study the rationality properties of our method in terms of unconditional and conditional query answering.

ABSTRACT. The topological μ-calculus has gathered attention in recent years as a powerful framework for representation of spatial knowledge. In particular, spatial relations can be represented over finite structures in the guise of weakly transitive (wK4) frames. In this paper we show that the topological μ-calculus is equivalent to a simple fragment based on a variant of the ‘tangle’ operator. Similar results were proven for more restricted classes of frames by Anuj Dawar and Martin Otto, using modal characterisation theorems for the corresponding classes of frames. However, since the μ-calculus is not equivalent to the bisimulation invariant fragment of FOL or of MSO over wK4 frames, we use a different method to prove our results; namely, the notion of finality which was also employed in the proof of completeness and FMP of the μ-calculus over wK4 frames. As a corollary we obtain a new proof of an existing result showing the collapse of the alternation hierarchy over wK4 frames.

ABSTRACT. In this paper, we introduce and study seven types of semantics for bipolar argumentation frameworks, each extending Dung's interpretation of attack with a distinct interpretation of support. First, we introduce three types of defence-based semantics by adapting the notions of defence. Second, we examine two types of selection-based semantics that select extensions by counting the number of supports. Third, we analyse two types of traditional reduction-based semantics under deductive and necessary interpretations of support. We provide full analysis of twenty-eight bipolar argumentation semantics and ten principles.

ABSTRACT. We address complex reasoning tasks in assumption-based argumentation (ABA) by developing dynamic programming algorithms based on tree-decompositions. As one of the prominent approaches in computational argumentation, our focus is on NP-hard reasoning in ABA. We utilize tree-width, a structural measure describing closeness to trees, for an approach to handle computationally complex tasks in ABA. We contribute to the state of the art by first showing that many reasoning tasks in ABA are fixed-parameter tractable w.r.t. tree-width using Courcelle's theorem, informally signaling wide applicability of dynamic programming algorithms for ABA. Secondly, we develop such algorithms operating on tree-decompositions of given ABA frameworks. We instantiate the algorithms in the recent D-FLAT framework allowing for declarative and extensible specification of dynamic programming algorithms. In an experimental evaluation on a resulting prototype we show promise of the approach in particular for complex counting tasks.

ABSTRACT. Some semantics for argumentation, including the newly introduced weakly admissible semantics, allow us to ignore attacks from arguments that are perceived as problematic. A key intuition motivating such semantics is that arguments that indirectly attack themselves may be problematic in such a way that this is justified. In this paper, we formalise this intuition and provide a class of semantics that are weakly admissible, coincide with the stable semantics on a large class of argumentation frameworks that admit stable sets, and only ignore attacks from arguments on unsafe cycles of odd length. We also show that no member of our class of semantics coincide with the semantics that takes all $\subseteq$-maximal weakly admissible sets as extensions. However, we show that this semantics satisfies an even stronger property, if the following conjecture is true: if an argumentation framework has no non-empty weakly admissible sets, then every argument lies on an unsafe odd cycle.

ABSTRACT. The expressiveness of any given formalism lays the theoretical foundation for more specialized topics, such as dynamics, believe change, etc. There, many (im-)possibility results can be directly inferred from the expressiveness. In this paper we investigate the expressiveness of assumption-based argumentation (ABA), one of the major formalisms of structured argumentation. In particular, we examine so-called signatures, i.e. sets of extensions that can be expressed under a given semantics. We characterize the signatures of common ABA semantics for flat, finite frameworks with and without preferences. Moreover, we present several observations regarding the expressiveness of conclusion-based semantics for ABA frameworks.

ABSTRACT. We propose a new approach based on Formal Concept Analysis (FCA) for computing stable extensions of Abstract Argumentation Frameworks (AFs). To this purpose we characterize an AF as a formal context, in which stable extensions of the AF are closed sets called concept intents. We make use of algorithms developed in FCA for computing concept intents in order to compute stable extensions of AFs. Our algorithms are easily extendable to preferred extensions. Experimental results show that on AFs with a high density of attacks-relation they perform significantly better than the existing approaches.

ABSTRACT. The need for AI applications to be explainable and trustworthy is eminently clear in domains where AI-supported decisions can have significant real-world consequences. The field of law is one such characteristic domain. In this talk I will present an overview of recent research investigating how different AI techniques can be combined to provide support for automating reasoning about legal cases in an efficient and explainable manner. Symbolic, logic-based techniques are used to represent the legal knowledge of a domain in a structured manner and machine learning techniques are used to identify the inputs to the symbolic model. The hybrid approach enables the different techniques to be targeted towards the particular tasks where they are most effective, within the overall automation pipeline. I will provide an overview of the hybrid system along with the first sets of results of experiments evaluating the performance of the hybrid system where the domain used is legal cases from the European Court of Human Rights.