ABSTRACT. Vadalog is a logic-based reasoning language for modern AI applications, in particular for knowledge graph systems. In this paper, we present recent advances and applications, with a focus on the language Vadalog itself. We first give an easy-to-access self-contained introduction to warded Datalog+/-, the logical core of Vadalog. We then discuss some recent advances: Datalog rewritability of warded Datalog+/-, and the piece-wise linear fragment of warded Datalog+/- that achieves space efficiency. We then proceed with some recent practical applications of the Vadalog language: detection of close links in financial knowledge graphs, as well as the detection of family-owned businesses.

ABSTRACT. We make a first step towards adapting an existing approach for privacy-preserving publishing of linked data to Description Logic (DL) ontologies. We consider the case where both the knowledge about individuals and the privacy policies are expressed using concepts of the DL EL, which corresponds to the setting where the ontology is an EL instance store. We introduce the notions of compliance of a concept with a policy and of safety of a concept for a policy, and show how optimal compliant (safe) generalizations of a given EL concept can be computed. In addition, we investigate the complexity of the optimality problem.

ABSTRACT. We continue our exploration of the relationships between Description Logics and Set Theory, which started with the definition of the description logic $\alc^\Omega$. We develop a set-theoretic translation of the description logic $\alc^\Omega$ in the set theory $\Omega$, exploiting a technique originally proposed for translating normal modal and polymodal logics into $\Omega$.

We first define a set-theoretic translation of $\alc$ based on Schild's correspondence with polymodal logics. Then we propose a translation of a fragment of $\alc^\Omega$ without roles and individual names. In this---simple---case the power-set concept is mapped, as expected, to the set-theoretic power-set, making clearer the real nature of the power-set concept in $\alc^\Omega$.Finally, we encode the whole language of $\alc^\Omega$ into its fragment without roles, showing that such a fragment is as expressive as $\alc^\Omega$. The encoding provides, as a by-product, a set-theoretic translation of $\alc^\Omega$ into the theory $\Omega$, which can be used as basis for extending other, more expressive, DL's with the power-set construct.

ABSTRACT. Description logics (DLs) are well known knowledge representation formalisms focused on the representation of terminological knowledge. A probabilistic extension of a light-weight DL was recently proposed for dealing with certain knowledge occurring in uncertain contexts. In this paper, we continue that line of research by introducing the Bayesian extension BALC of the DL ALC. We present a tableau-based procedure for deciding consistency, and adapt it to solve other probabilistic, contextual, and general inferences in this logic. We also show that all these problems remain ExpTime-complete, as reasoning in the underlying classical ALC.

ABSTRACT. We present ALC^ME, a probabilistic variation of the Description Logic ALC that allows for representing and processing conditional statements of the form "if A holds, then B follows with probability p" under the principle of maximum entropy. Probabilities are understood as degrees of belief and formally interpreted by the aggregating semantics. A major problem for probabilistic reasoning from such conditional knowledge bases is to count models and individuals. We prove that both checking consistency and drawing inferences based on approximations of the maximum entropy distribution is possible in ALC^ME in time polynomial in the domain size. For this, we develop sophisticated counting strategies to aggregate interpretations with respect to the so-called conditional impacts of types which refine their conditional structure.

ABSTRACT. We investigate the problem of learning description logic ontologies from entailments via queries, using epistemic reasoning. We introduce a new learning model consisting of epistemic membership and example queries and show that polynomial learnability in this model coincides with polynomial learnability in Angluin’s exact learning model with membership and equivalence queries. We then instantiate our learning framework to EL and show some complexity results for an epistemic extension of EL where epistemic operators can be applied over the axioms. Finally, we transfer known results for EL ontologies and its fragments to our learning model based on epistemic reasoning.

ABSTRACT. For the development of large-scale representations of knowledge the application of methodologies and design principles becomes relevant. The knowledge may be organized in ontologies in a modular and hierarchical fashion. An upper-level ontology typically provides specifications of requirements, functions, design or standards that are to be complied with by domain ontologies on a lower level in the hierarchy. Verifying whether and how specifications have been implemented by domain ontologies becomes a challenge when relevant axioms of the domain ontology need to be inspected. We consider specifications to be defined using entailments of certain queries over a given vocabulary. For selecting the relevant axioms, we propose a novel module notion called projection module that entails the queries that follow from a reference ontology. We develop algorithms for computing minimal projection modules of Description Logic terminologies for subsumption, instance and conjunctive queries.

ABSTRACT. Description logics in their standard setting only allow for representing and reasoning with crisp knowledge without any degree of uncertainty. Of course, this is a serious shortcoming for use cases where it is impossible to perfectly determine the truth of a statement. For resolving this expressivity restriction, probabilistic variants of description logics have been introduced. Their model-theoretic semantics is built upon so-called probabilistic interpretations, that is, families of directed graphs the vertices and edges of which are labeled and for which there exists a probability measure on this graph family.

Results of scientific experiments, e.g., in medicine, psychology, or biology, that are repeated several times can induce probabilistic interpretations in a natural way. In this document, we shall develop a suitable axiomatization technique for deducing terminological knowledge from the assertional data given in such probabilistic interpretations. More specifically, we consider a probabilistic variant of the description logic ℰℒ, and provide a method for constructing a set of rules, so-called concept inclusions, from probabilistic interpretations in a sound and complete manner.

ABSTRACT. We present a general logical framework for reasoning about agents' cognitive attitudes of both epistemic type and motivational type. We provide a sound and complete axiomatization for our logic and we show that it allows us to express a variety of relevant concepts for qualitative decision theory including the concepts of knowledge, belief, strong belief, conditional belief, desire, strong desire, comparative desirability and choice.

ABSTRACT. Modal separation logics are formalisms that combine modal operators to reason locally with separating connectives that allow to perform global updates on the models. In this work, we design Hilbert-style proof systems for the modal separation logics MSL(*,<\neq>) and MSL(*,<>) where * is the separating conjunction, <> is the standard modal operator and <\neq> is the difference modality. The calculi only use the logical languages at hand (no external features such as labels) and take advantage of new normal forms and of their axiomatisation.

ABSTRACT. A complete classification of the complexity of the local and global satisfiability problems for graded modal language over traditional classes of frames has already been established. By ''traditional'' classes of frames we mean those characterized by any positive combination of reflexivity, seriality, symmetry, transitivity, and the Euclidean property. In this paper we fill the gaps remaining in an analogous classification of the graded modal language with graded converse modalities. In particular we show its NExpTime-completeness over the class of Euclidean frames, demonstrating this way that over this class the considered language is harder than the language without graded modalities or without converse modalities. We also consider its variation disallowing graded converse modalities, but still admitting basic converse modalities. Our most important result for this variation is confirming an earlier conjecture that it is decidable over transitive frames. This contrasts with the undecidability of the language with graded converse modalities.

ABSTRACT. The logic of conditional belief, called Conditional Doxastic Logic (CDL), has been proposed by Board, Baltag and Smets to model revisable belief and knowledge in a multi-agent setting. We present a proof system for CDL in the form of a nested sequent calculus. To the best of our knowledge, ours is the first internal and standard calculus for this logic. The calculus is defined by taking as primitive a multi-agent version of the comparative plausibility operator, as in Lewis' counterfactual logic. The calculus is analytic and provides a decision procedure for CDL. As a by-product we also obtain a nested sequent calculus for multi-agent modal logic S5.

ABSTRACT. We investigate interpolation and Beth definability in Default Logics. To this end, we start by defining a general framework which is sufficiently abstract to encompass most of the usual definitions of Default Logics. Our definition of a default logic $\DefaultLogic$ is built on a base, monotonic, logic $\Logic$. We then investigate the question of when interpolation and Beth definability results transfer from $\Logic$ to $\DefaultLogic$. This investigation needs suitable notions of interpolation and Beth definability for Default Logics. We show both positive and negative general results: depending on how $\DefaultLogic$ is defined and of the kind of interpolation/Beth definability involved, the property might or might not transfer from $\Logic$ to $\DefaultLogic$.

ABSTRACT. We show that the satisfiability problem in core fragments of modal logics T, K4, and S4 in whose languages diamond modal operators are disallowed is NLogSpace-complete. Moreover, we provide deterministic procedures for satisfiability checking. We show that the above fragments correspond to certain core fragments of linear temporal logic, hence our results imply NLogSpace-completeness of the latter.

ABSTRACT. In classical deterministic planning, solutions to planning tasks are simply sequences of actions, but that is not sufficient for contingent plans in non-deterministic environments. Contingent plans are often expressed through policies that map states to actions. An alternative is to specify contingent plans as programs, e.g. in the syntax of Propositional Dynamic Logic (PDL). PDL is a logic for reasoning about programs with sequential composition, test and non-deterministic choice. However, as we show in the paper, none of the existing modalities in PDL capture the notion of a solution to a planning task under non-determinism. In the paper, we add a new modality to star-free PDL correctly capturing this notion. We prove the appropriateness of the new modality by showing how to translate back and forth between policies and PDL programs under the new modality. More precisely, we show how a policy solution to a planning task gives rise to a program solution expressed via the new modality, and vice versa. We also provide an axiomatisation of our PDL extension and prove some basic properties of it.

ABSTRACT. The relation between agentive action, knowledge, and obligation is central to the understanding of responsibility. Based on the view that an appropriate formalization of said relation would contribute to the development of ethical AI, we point out the main characteristics of a logic for objective and subjective oughts that was recently introduced in the literature. This logic extends the traditional stit paradigm with deontic and epistemic operators, and provides a semantics that deals with Horty's puzzles for knowledge and obligation. We provide an axiomatization for this logic, and address its soundness and completeness with respect to a class of relevant models.

ABSTRACT. The importance of intuitionistic temporal logics in Computer Science and Artificial Intelligence has become increasingly clear in the last few years. From the proof-theory point of view, intuitionistic temporal logics have made it possible to extend functional languages with new features via type theory, while from its semantical perspective several logics for reasoning about dynamical systems and several semantics for logic programming have their roots on this framework. In this paper we propose four axiomatic systems for intuitionistic linear temporal logic and show that each of these systems is sound for a class of structures based either on Kripke frames or on dynamic topological systems. Our topological semantics features a new interpretation for the `henceforth' modality that is a natural intuitionistic variant of the classical one. Using the soundness results, we show that the four logics obtained from the axiomatic systems are distinct.

ABSTRACT. Decision trees are simple, yet powerful, classification models used to classify categorical and numerical data, and, despite their sim- plicity, they are commonly used in operations research and management, as well as in knowledge mining. From a logical point of view, a decision tree can be seen as a structured set of logical rules written in proposi- tional logic. Since knowledge mining is rapidly evolving towards temporal knowledge mining, and since in many cases temporal information is best described by interval temporal logics, propositional logic decision trees may evolve towards interval temporal logic decision trees. In this paper, we define the problem of interval temporal logic decision tree learning, and propose a solution that generalizes classical decision tree learning.

ABSTRACT. We present cut-free labelled sequent calculi for a central formalism in logics of agency: STIT logics with temporal operators. These include sequent systems for Ldm, Tstit and Xstit. All calculi presented possess essential structural properties such as contraction- and cut-admissibility. The labelled calculi G3Ldm and G3Tstit are shown sound and complete w.r.t. irreflexive temporal frames. As a corollary, we extend current results by showing that also Xstit can be characterized through relational frames, omitting the use of BT+AC frames.

ABSTRACT. The stable-model semantics has been generalised from logic programs to arbitrary theories. We explore a further generalisation and consider sequences of atoms as models instead of sets. The language is extended by suitable order operators to access this additional information. We recently introduced an extension of classical logic by a single order operator with a temporal interpretation for activity reasoning. The logic envisaged here is a nonmonotonic version thereof. Our definition of what we call stable-ordered models is based on the stable-model semantics for theories due to Ferraris and Lifschitz with the necessary changes. Compared to related nonmonotonic versions of temporal logics, our approach is less costly as checking model existence remains at the second level of the polynomial hierarchy. We demonstrate versatile applications from activity reasoning, combinatorial testing, debugging concurrent programs, and digital forensics.