ABSTRACT. We show that the vast majority of extensions of the description logic EL do not enjoy the Craig interpolation nor the projective Beth definability property. This is the case, for example, for EL with nominals, EL with the universal role, EL with a role hierarchies and transitive roles, and for ELI. It follows, in particular, that the existence of an explicit definition of a concept or individual name cannot be reduced to subsumption checking via implicit definability. We show that nevertheless the existence of interpolants and explicit definitions can be decided in polynomial time for standard tractable extensions of EL (such as EL++) and in ExpTime for ELI and various extensions. It follows that these existence problems are not harder than subsumption which is in sharp contrast to the situation for expressive DLs. We also obtain tight bounds for the size of interpolants and explicit definitions and the complexity of computing them: single exponential for tractable standard extensions of EL and double exponential for ELI and extensions. We close with a discussion of Horn-DLs such as Horn-ALCI.

ABSTRACT. PL is a low-complexity profile of OWL2, expressly designed in the H2020 project SPECIAL to encode data usage policies and personal data protection regulations - such as the GDPR - in a machine understandable way. With PL, the compliance of privacy policies with the GDPR and with the data subjects' consent to processing can be checked automatically and in real time. The followup H2020 project TRAPEZE is extending PL to support richer policies, including "sticky policies". They are a sort of license that applies to data transfers, and specifies how the recipient can use the data. Sticky policies may be "recursive", i.e. they may apply not only to the first data transfer, but also to all subsequent transfer operations that the (direct or indirect) recipients may execute in the future. Such recursive sticky policies may be encoded with fixpoints or transitive role closure. In this paper we prove that such extensions make compliance checking intractable. Since the scalability of compliance checking is a major requirement in this area, these results justify an ad-hoc, low complexity approach to encoding sticky policies.

ABSTRACT. Ontologies based on Description Logic (DL) represent general background knowledge in a terminology (TBox) and the actual data in an ABox. DL systems can then be used to compute consequences (such as answers to certain queries) from an ontology consisting of a TBox and an ABox. Since both human-made and machine-learned data sets may contain errors, which manifest themselves as unintuitive or obviously incorrect consequences, repairing DL-based ontologies in the sense of removing such unwanted consequences is an important topic in DL research. Most of the repair approaches described in the literature produce repairs that are not optimal, in the sense that they do not guarantee that only a minimal set of consequences is removed. In a series of papers, we have developed an approach for computing optimal repairs, starting with the restricted setting of an EL instance store, extending this to the more general setting of a quantified ABox (where some individuals may be anonymous), and then adding a static EL TBox.

Here, we extend the expressivity of the underlying DL considerably, by adding nominals, inverse roles, regular role inclusions and the bottom concept to EL, which yields a fragment of the well-known DL Horn-SROIQ. The ideas underlying our repair approach still apply to this DL, though several non-trivial extensions are needed to deal with the new constructors and axioms. The developed repair approach can also be used to treat unwanted consequences expressed by certain conjunctive queries or regular path queries, and to handle Horn-ALCOI TBoxes with regular role inclusions.

ABSTRACT. We investigate practical algorithms for inconsistency-tolerant query answering over prioritized knowledge bases, which consist of a logical theory, a set of facts, and a priority relation between conflicting facts. We consider three well-known semantics (AR, IAR and brave) based upon two notions of optimal repairs (Pareto and completion). Deciding whether a query answer holds under these semantics is (co)NP-complete in data complexity for a large class of logical theories, and SAT-based procedures have been devised for repair-based semantics when there is no priority relation, or the relation has a special structure. The present paper introduces the first SAT encodings for Pareto- and completion-optimal repairs w.r.t. general priority relations and proposes several ways of employing existing and new encodings to compute answers under (optimal) repair-based semantics, by exploiting different reasoning modes of SAT solvers. The comprehensive experimental evaluation of our implementation compares both (i) the impact of adopting semantics based on different kinds of repairs, and (ii) the relative performances of alternative procedures for the same semantics.

ABSTRACT. We introduce Forecasting Argumentation Frameworks (FAFs), a novel argumentation-based methodology for forecasting informed by recent judgmental forecasting research. FAFs comprise update frameworks which empower (human or artificial) agents to argue over time about the probability of outcomes, e.g. the winner of an election or a fluctuation in inflation rates, whilst flagging perceived irrationality in the agents' behaviour with a view to improving their forecasting accuracy. FAFs include five argument types, amounting to standard pro/con arguments, as in bipolar argumentation, as well as novel proposal arguments and increase/decrease amendment arguments. We adapt an existing gradual semantics for bipolar argumentation to determine the aggregated dialectical strength of proposal arguments and define irrational behaviour. We then give a simple aggregation function which produces a final group forecast from rational agents' individual forecasts. We identify and study properties of FAFs, and conduct an empirical evaluation which signals FAFs' potential to increase the forecasting accuracy of participants.

ABSTRACT. We present the system ALASPO which implements Adaptive Large-neighbourhood search for Answer Set Programming (ASP) Optimisation. Large-neighbourhood search (LNS) is a meta heuristic where parts of a solution are destroyed and reconstructed in an attempt to improve an overall objective. ALASPO currently supports the ASP solver clingo, as well as its extensions clingo-dl and clingcon for difference and full integer constraints, and multi-shot solving for an efficient implementation of the LNS loop. Neighbourhoods can be defined in code or declaratively as part of the ASP encoding, and they can be used in a portfolio together with differ-ent search configurations. Switching can be done on the fly during search, or the system can be run in full self-adaptive modes. To demonstrate the benefits of adaptive LNS for ASP, we evaluate ALASPO on different optimisation benchmarks, thereby complementing previous work.

ABSTRACT. Datalog^E is the extension of Datalog with existential quantification. While its high expressive power, underpinned by a simple syntax and the support for full recursion, renders it particularly suitable for modern applications on Knowledge Graphs, query answering (QA) over such language is known to be undecidable in general. For this reason, different fragments have emerged, introducing syntactic limitations to Datalog^E that strike a balance between its expressive power and the computational complexity of QA, to achieve decidability. In this short paper, we focus on two promising tractable candidates, namely Shy and Warded Datalog+/-. Reacting to an explicit interest from the community, we shed light on the relationship between these fragments. Moreover, we carry out an experimental analysis of the systems implementing Shy and Warded, respectively DLV^E and Vadalog.

ABSTRACT. We study the problem of performing reasoning with existential rules on streams of data for query answering about the present and future. Although reasoning with existential rules is a problem that has been widely studied (e.g., see chasing algorithms), current works mainly focused on static data and we are not aware on any extension to streams of data. To cover this gap, we considered LARS, currently one of the most prominent frameworks for rule-based stream reasoning. LARS is an ideal starting point because it offers many stream operators (e.g., windowing), but it does not support value invention. To remove this limitation, we show how we can extend LARS with existentially quantified variables, introduce a procedure to translate LARS reasoning into a set of existential rules, and describe how we can leverage the temporal nature of the stream to implement stronger acyclicity notions. Our contribution also includes a preliminary experimental evaluation over artificial streams.

ABSTRACT. In multi-agent belief fusion, there is increasing interest in results and methods from social choice theory. As a theoretical cornerstone, the Condorcet Jury Theorem (CJT) states that given a number of equally competent, independent agents where each is more likely to guess the true out of two alternatives, the chances of determining this objective truth by majority voting increase with the number of participating agents, approaching certainty. Past generalizations of the CJT have shown that some of its underlying assumptions can be weakened. Motivated by requirements from practical belief fusion scenarios, we provide a significant further generalization that subsumes several of the previous ones. Our considered setting simultaneously allows for heterogeneous competence levels across the agents (even tolerating entirely incompetent or even malicious voters), and voting for any number of alternatives from a finite set. We derive practical lower bounds for the numbers of agents needed to give probabilistic guarantees for determining the true state through approval voting. We also demonstrate that the non-asymptotic part of the CJT fails in our setting for arbitrarily high numbers of voters.

ABSTRACT. This paper introduces a novel method for merging open-domain terminological knowledge. It takes advantage of the Region Connection Calculus (RCC5), a formalism used to represent regions in a topological space and to reason about their set-theoretic relationships. To this end, we first propose a faithful translation of terminological knowledge provided by several and potentially conflicting sources into region spaces. The merging is then performed on these spaces, and the result is translated back into the underlying language of the input sources. Our approach allows us to benefit from the expressivity and the flexibility of RCC5 while dealing with conflicting knowledge in a principled way.

ABSTRACT. In a recent paper, we presented a Situation Calculus-based framework for modelling an agent that has incomplete or inaccurate knowledge about its environments, whose actions are non-deterministic, and whose sensor might give incorrect results. Generalizing earlier proposals, the presented approach represented the agent's epistemic state by a set of situations ranked by their respective plausibility, which would then be updated by modifying the plausibility ranks accordingly. Two notions of belief were distinguished, an extensional "bird's eye" view on the one hand, and an intensional one on the other hand, where beliefs are represented from the agent's perspective. In this short paper, we extend our earlier work by considering the problem of projection in this framework, i.e. the question whether a certain (epistemic) formula will hold after a given sequence of actions. We present results on both regression, where the query is transformed into an equivalent one about the initial situation, as well as progression, where the knowledge base is updated to reflect the situation after executing the action sequence in question.

ABSTRACT. In this paper, we investigate inductive inference with system W from conditional belief bases with respect to syntax splitting. The concept of syntax splitting for inductive inference states that inferences about independent parts of the signature should not affect each other. This was captured in work by Kern-Isberner, Beierle, and Brewka in the form of postulates for inductive inference operators expressing syntax splitting as a combination of relevance and independence; it was also shown that c-inference fulfils syntax splitting, while system P inference and system Z both fail to satisfy it. System W is a recently introduced inference system for nonmonotonic reasoning that captures and properly extends system Z as well as c-inference. We show that system W fulfils the syntax splitting postulates for inductive inference operators by showing that it satisfies the required properties of relevance and independence. This makes system W another inference operator besides c-inference that fully complies with syntax splitting, while in contrast to c-inference, also extending rational closure.

ABSTRACT. Iterated Belief Change is the research area that investigates principles for the dynamics of beliefs over (possibly unlimited) many subsequent belief changes. In this paper, we demonstrate how iterated belief change is connected to computation. In particular, we show that iterative belief revision is Turing complete, even under the condition that broadly accepted principles like the Darwiche-Pearl postulates for iterated revision hold.

ABSTRACT. We study the problem to decide, given sets T1, T2 of TGDs (also called existential rules), whether T2 is a conservative extension of T1. We consider two natural notions of conservative extension, one pertaining to answers to conjunctive queries over databases and one to homomorphisms between chased databases. Our main results are that these problems are undecidable for linear TGDs, undecidable for guarded TGDs even when T1 is empty, and decidable for frontier-one TGDs.

ABSTRACT. Data provenance consists in bookkeeping meta information during query evaluation, in order to enrich query results with their trust level, likelihood, evaluation cost, and more. The framework of semiring provenance abstracts from the specific kind of meta information that annotates the data. While the definition of semiring provenance is uncontroversial for unions of conjunctive queries, the picture is less clear for Datalog. Indeed, the original definition might include infinite computations, and is not consistent with other proposals for Datalog semantics over annotated data. In this work, we propose and investigate several provenance semantics, based on different approaches for defining classical Datalog semantics. We study the relationship between these semantics, and introduce properties that allow us to analyze and compare them.

ABSTRACT. Existential rules are an expressive knowledge representation language mainly developed to query data. In the literature, they are often supposed to be in some normal form that simplifies technical developments. For instance, a common assumption is that rule heads are atomic, i.e., restricted to a single atom. Such assumptions are considered to be made without loss of generality as long as all sets of rules can be normalised while preserving entailment. However, an important question is whether the properties that ensure the decidability of reasoning are preserved as well. We provide a systematic study of the impact of these procedures on the different chase variants with respect to chase (non-)termination and FO-rewritability. This also leads us to solve open problems related to chase termination of independent interest.

ABSTRACT. Interest in non-monotonic reasoning arose from the need to model how people in everyday life use defeasible knowledge (i.e. knowledge that is normally correct but can have exceptions). One path of research that has evolved from this is computational models of argument. This is concerned with modelling the human ability to handle incomplete and conflicting situations through the identification and analysis of arguments and counterarguments. A key problem in computational models of argument is the need to handle enthymemes. These are arguments that have some premises, and possibly the claim, being implicit. To understand enthymemes, for example exchanged during a dialogue, we often require commonsense reasoning. Whilst the need to formalise commonsense reasoning was a driver for research in non-monotonic reasoning, the questions of how to formalise commonsense reasoning, and how to acquire the knowledge necessary for commonsene reasoning, remain largely unanswered. In this talk, we will review the fields of non-monotonic reasoning, computational models of argument, and commonsense reasoning, and focus on the handling of enthymemes.

ABSTRACT. Several approaches have been developed for answering users' specific questions about AI behavior and for assessing their core functionality in terms of primitive executable actions. However, the problem of summarizing an AI agent's broad capabilities for a user is comparatively new. This paper presents an algorithm for discovering from scratch the suite of high-level "capabilities" that an AI system with arbitrary internal planning algorithms/policies can perform. It computes conditions describing the applicability and effects of these capabilities in user-interpretable terms. Starting from a set of user-interpretable state properties, an AI agent, and a simulator that the agent can interact with, our algorithm returns a set of high-level capabilities with their parameterized descriptions. Empirical evaluation on several game-based scenarios shows that this approach efficiently learns descriptions of various types of AI agents in deterministic, fully observable settings. User studies show that such descriptions are easier to understand and reason with than the agent's primitive actions.

ABSTRACT. In this paper, we introduce and study a dynamic deontic logic for permitted announcements. In our logic framework, it is permitted to announce $\phi$ if announcing $\phi$ would not lead to forbidden knowledge. It is shown that the logic is not compact, and we propose a sound and weakly complete Hilbert-style axiomatisation. We also study the computational complexity of the model checking problem and the decidability of the satisfiability problem. Finally, we introduce a neighbourhood semantics with a strongly complete axiomatisation

ABSTRACT. Rule learning from large datasets has regained extensive interest as rules are useful for developing explainable approaches to many applications in knowledge graphs. However, existing methods for rule learning are still limited in terms of scalability and rule quality. This paper presents a new method for learning typed rules by employing entity class information. Our experimental evaluation shows the superiority of our system compared to state-of-the-art rule learners. In particular, we demonstrate the usefulness of typed rules in reasoning for link prediction.

ABSTRACT. General Game Playing (GGP) aims to develop agents that are able to play any game with only rules given. The game rules are encoded in the Game Description Language (GDL). A GGP player processes the game rules to obtain game states and expand the game tree search for an optimal move. The recent accomplishments of AlphaGo and AlphaZero have triggered new works in extending neural network approaches to GGP. In these works, the neural networks are used only for optimal move selection, while the components dealing with GDL still use logic-based methods. This motivates us to explore if a neural network based method would be able to approximate the logical inference in GDL with a high accuracy. The structured nature of logic tends to be a difficulty for neural networks, which rely heavily on statistical features. Inspired by the recent works on neural network learning for logical entailments, we propose a neural network based reasoner that is able to learn logical inferences for GDL. We present three key contributions: (i) a general, game-agnostic graph-based representation for game states described in GDL, (ii) methods for generating samples and datasets to frame the GDL inference task as a neural network based machine learning problem and (iii) a GNN based neural reasoner that is able to learn and infer various game states with a high accuracy and has some capability of transfer learning across games.

ABSTRACT. Causal models are playing an increasingly important role in machine learning, particularly in the realm of explainable AI. We introduce a conceptualisation for generating argumentation frameworks (AFs) from causal models for the purpose of forging explanations for the models’ outputs. The conceptualisation is based on reinterpreting desirable properties of semantics of AFs as explanation moulds, which are means for characterising argumentatively the relations in the causal model. We demonstrate our methodology by reinterpreting the property of Bi-variate Reinforcement as an explanation mould to forge bipolar AFs as explanations for the outputs of causal models. We perform a theoretical evaluation of these argumentative explanations, examining whether they satisfy a range of desirable explanatory and argumentative properties.

ABSTRACT. In this paper we contribute to the investigation of dynamics in assumption-based argumentation (ABA) and investigate situations where a given knowledge base undergoes certain changes. We show that two frequently investigated problems, namely enforcement of a given target atom and deciding strong equivalence of two given ABA frameworks, are NP-complete in general. Interestingly, these problems are both tractable for abstract argumentation frameworks (AFs) which admit a close correspondence to ABA by constructing semantics-preserving instances. Inspired by this observation, we search for tractable fragments for ABA frameworks by means of the instantiated AFs. We argue that the usual instantiation procedure is not suitable for the investigation of dynamic scenarios since too much information is lost when constructing the AF. We thus consider an extension of AFs, called cvAFs, equipping arguments with conclusions and vulnerabilities in order to better anticipate their role after the underlying knowledge base is extended. We investigate enforcement and strong equivalence for cvAFs and present syntactic conditions to decide them. We show that the correspondence between cvAFs and ABA frameworks is close enough to capture ABA also in dynamic scenarios. This yields the desired tractable ABA fragment. We furthermore discuss consequences for the corresponding problems for logic programs.

ABSTRACT. We propose a general framework to investigate semantics of Dung-style argumentation frameworks (AFs) by means of generic defeat operators. After establishing the technical foundations, we propose natural generic versions of Dung's classical semantics. We demonstrate how classical as well as recent proposals can be captured by our approach when utilizing suitable notions of defeat. We perform an investigation of basic properties which semantics inherit from the underlying defeat operator. In particular, we show under which conditions a counterpart to Dung's fundamental lemma can be inferred and how it ensures the existence of the generalized version of complete extensions. We contribute to a principle-based study of AF semantics by discussing properties tailored to compare different defeat operators. Finally, we report computational complexity results which hold in our general framework.

ABSTRACT. KR 2022 Closing slides, announcing KR 2023