We study an epistemic logic where knowledge is built from what the agents observe (including higher-order visibility) and what the agents learn from public announcements. This fixes two main drawbacks of previous observability-based approaches where who sees what is common knowledge and where the epistemic operators distribute over disjunction. The latter forbids the modeling of most of the classical epistemic problems, starting with the muddy children puzzle. We integrate a dynamic dimension where both facts of the world and the agents’ observability can be modified by assignment programs. We establish that the model checking problem is PSPACE-complete.

In temporal logics, the operator F expresses that at some time in the future something happens, e.g., a request is eventually granted. Unfortunately, there is no bound on the time un- til the eventuality is satisfied which in many cases does not correspond to the intuitive meaning system designers have, namely, that F abstracts the idea that there is a bound on this time although its magnitude is not known. An elegant way to capture this meaning is through Prompt-LTL, which extends LTL with the operator F P ("prompt eventually"). We extend this work by studying alternating-time epistemic temporal logics extended with F P . We study the model-checking problem of the logic Prompt- KATL∗, which is ATL∗ extended with epistemic operators and prompt eventually. We also obtain results for the model-checking problem of some of its fragments. Namely, of Prompt-KATL (ATL with epistemic operators and prompt eventually), Prompt-KCTL∗ (CTL∗ with epistemic operators and prompt eventually), and finally the existential fragments of Prompt-KATL∗ and Prompt-KATL.

Recently, the field of knowledge representation is drawing a lot of inspiration from database theory. In particular, in the area of description logics and ontology languages, interest has shifted from satisfiability checking to query answering, with various query notions adopted from databases, like (unions of) conjunctive queries or different kinds of path queries. Likewise, the finite model semantics is being established as a viable and interesting alternative to the traditional semantics based on unrestricted models. In this paper, we investigate diverse database-inspired reasoning problems for very expressive description logics (all featuring the worrisome trias of inverses, counting, and nominals) which have in common that role paths of unbounded length can be described (in the knowledge base or of the query), leading to a certain non-locality of the reasoning problem. We show that for all the cases considered, undecidability can be established by very similar means. Most notably, we show undecidability of finite entailment of unions of conjunctive queries for a fragment of SHOIQ (the logic underlying the OWL DL ontology language), and undecidability of finite entailment of conjunctive queries for a fragment of SROIQ (the logical basis of the more recent and popular OWL 2 DL standard).

Some applications of Description Logic (DL) ontologies combine complete information (e.g., stemming from relational databases) with incomplete, open-world knowledge. Several research efforts in the last years have advocated closed predicates, which are predicates whose extension is interpreted as complete, as a suitable way to leverage partial completeness within the standard open-world semantics of DLs. These works have also studied the data complexity of query answering in the presence of closed predicates, which is generally intractable. In this paper we contribute to the understanding the combined complexity of the problem, by establishing tight complexity results for a range of DLs and query answering problems. In summary, our results show that consistency testing and instance query answering in the presence of closed predicates are feasible in NP even for rich dialects of the DL-Lite family; this is the lowest complexity that could be expected. For EL, in contrast, they are EXPTIME-complete, thus as hard as for ALC and some of its extensions. If unions of conjunctive queries (UCQs) are considered, the picture is even bleaker: we can show 2EXPTIME-hardness even for DL-Lite_R and EL. This is in sharp contrast to the NP-upper bound in the standard setting without closed predicates, and coincides with known upper bounds for much richer DLs. We note that our results imply 2EXPTIME-hardness of query answering in ALCO for the standard setting, where all predicates are interpreted under the open-world semantics. This singles out nominals as a previously unidentified source of complexity when answering queries over expressive DLs. Despite these negative results, we can still identify several useful classes of queries for which the increase in hardness is not as drastic, and the combined complexity of query answering remains between NP and coNEXPTIME.

We study anti-unification for the description logic EL and introduce thenotion of least general generalisation, which generalises simultaneously leastcommon subsumer and concept matching. The idea of generalisation of twoconcepts is to detect maximal similarities between them, and to abstract overtheir differences uniformly. We demonstrate that a finite minimal complete setof generalisations for ELconcepts always exists and establish complexitybounds for computing them. Wepresent an anti-unification algorithm that computes generalisations with afixed skeleton, study its properties and report on preliminary experimental evaluation.

Ontology alignment (also called ontology matching) is the process of identifying correspondences between entities in different, possibly heterogeneous, ontologies. Traditional ontology alignment techniques rely on the full disclosure of the ontological models; however, within open and opportunistic environments, such approaches may not always be pragmatic or even acceptable (due to privacy concerns). Several studies have focussed on collaborative, decentralised approaches to ontology alignment, where agents negotiate the acceptability of single correspondences acquired from past encounters, or try to ascertain novel correspondences on the fly. However, such approaches can lead to logical violations that may undermine their utility. In this paper, we extend a dialogical approach to correspondence negotiation, whereby agents not only exchange details of possible correspondences, but also identify potential violations to the consistency and conservativity principles. We present a formal model of the dialogue, and show how agents can repair logical violations during the dialogue by invoking a correspondence repair, thus negotiating and exchanging repair plans. We illustrate this opportunistic alignment mechanism with an example and we empirically show that allowing agents to strategically reject or weaken correspondences when these cause violations does not degrade the effectiveness of the alignment computed, whilst reducing the number of residual violations.

We study query containment in three closely related formalisms: monadic disjunctive Datalog (MDDLog), MMSNP (a logical generalization of constraint satisfaction problems), and ontology-mediated queries (OMQs) based on expressive description logics and unions of conjunctive queries. Containment in MMSNP was known to be decidable due to a result by Feder and Vardi, but its exact complexity has remained open. We prove 2NExpTime-completeness and extend this result to monadic disjunctive Datalog and to OMQs.

An ontology-based data access (OBDA) system is composed of one or more data sources, an ontology that provides a conceptual view of the data, and declarative mappings that relate the data and ontology schemas. In order to debug and optimize such systems, it is important to be able to analyze and compare OBDA specifications. Recent work in this direction compared specifications using classical notions of equivalence and entailment, but an interesting alternative is to consider query-based notions, in which two specifications are deemed equivalent if they give the same answers to the considered query or class of queries for all possible data sources. In this paper, we define such query-based notions of entailment and equivalence of OBDA specifications and investigate the complexity of the resulting analysis tasks when the ontology is formulated in (fragments of) DL-Lite R .

Consequence-based calculi are a family of reasoning algorithms for description logics (DLs), and they combine hypertableau and resolution in a way that often achieves excellent performance in practice. Up to now, however, they were proposed for either Horn DLs (which do not support disjunction), or for DLs without counting quantifiers. In this paper we present a novel consequence-based calculus for SRIQ — a rich DL that supports both features. This extension is non-trivial since the intermediate consequences that need to be derived during reasoning cannot be captured using DLs themselves. The results of our preliminary performance evaluation suggest the feasibility of our approach in practice.

We review several different languages for collective decision making problems, in which agents express their judgments, opinions, or beliefs over elements of a logically structured domain. Several such languages have been proposed in the literature to compactly represent the questions on which the agents are asked to give their views. In particular, the framework of judgment aggregation allows agents to vote directly on complex, logically related formulas, whereas the setting of binary aggregation asks agents to vote on propositional variables, over which dependencies are expressed by means of an integrity constraint. We compare these two languages and some of their variants according to their relative succinctness and according to the computational complexity of aggregating several individual views expressed in such languages into a collective judgment. Our main finding is that the formula-based language of judgment aggregation is more succinct than the constraint-based language of binary aggregation. In many (but not all) practically relevant situations, this increase in succinctness does not entail an increase in complexity of the corresponding problem of computing the outcome of an aggregation rule.