
Our concern is the completeness problem for spilogics, that is, sets of
implications between strictly positive formulas built from propositional
variables, conjunction and modal diamond operators. Originated in logic,
algebra and computer science, spilogics have two natural semantics:
meetsemilattices with monotone operators providing Birkhoffstyle calculi, and
firstorder relational structures (aka Kripke frames) often used as the
intended structures in applications. Here we lay foundations for a completeness
theory that aims to answer the question whether the two semantics define the
same consequence relations for a given spilogic.

We propose a novel framework for ontologybased access to temporal log data
using a datalog extension datalogMTL of a Horn fragment of the metric temporal
logic MTL. We show that datalogMTL is ExpSpacecomplete even with punctual
intervals, in which case full MTL is known to be undecidable. We also prove
that nonrecursive datalogMTL is PSpacecomplete for combined complexity and in
AC0 for data complexity. We demonstrate by two realworld use cases that
nonrecursive datalogMTL programs can express complex temporal concepts from
typical user queries and thereby facilitate access to temporal log data. Our
experiments with Siemens turbine data and MesoWest weather data show that
datalogMTL ontologymediated queries are efficient and scale on large datasets.

The question whether an ontology can safely be replaced by another, possibly
simpler, one is fundamental for many ontology engineering and maintenance
tasks. It underpins, for example, ontology versioning, ontology modularization,
forgetting, and knowledge exchange. What safe replacement means depends on the
intended application of the ontology. If, for example, it is used to query
data, then the answers to any relevant ontologymediated query should be the
same over any relevant data set; if, in contrast, the ontology is used for
conceptual reasoning, then the entailed subsumptions between concept
expressions should coincide. This gives rise to different notions of ontology
inseparability such as query inseparability and concept inseparability, which
generalize corresponding notions of conservative extensions. We survey results
on various notions of inseparability in the context of description logic
ontologies, discussing their applications, useful modeltheoretic
characterizations, algorithms for determining whether two ontologies are
inseparable (and, sometimes, for computing the difference between them if they
are not), and the computational complexity of this problem.

We investigate the satisfiability problem for Horn fragments of the
HalpernShoham interval temporal logic depending on the type (box or diamond)
of the interval modal operators, the type of the underlying linear order
(discrete or dense), and the type of semantics for the interval relations
(reflexive or irreflexive). For example, we show that satisfiability of Horn
formulas with diamonds is undecidable for any type of linear orders and
semantics. On the contrary, satisfiability of Horn formulas with boxes is
tractable over both discrete and dense orders under the reflexive semantics and
over dense orders under the irreflexive semantics, but becomes undecidable over
discrete orders under the irreflexive semantics. Satisfiability of binary Horn
formulas with both boxes and diamonds is always undecidable under the
irreflexive semantics.

Our concern is the overhead of answering OWL 2 QL ontologymediated queries
(OMQs) in ontologybased data access compared to evaluating their underlying
treeshaped and bounded treewidth conjunctive queries (CQs). We show that OMQs
with boundeddepth ontologies have nonrecursive datalog (NDL) rewritings that
can be constructed and evaluated in LOGCFL for combined complexity, even in NL
if their CQs are treeshaped with a bounded number of leaves, and so incur no
overhead in complexitytheoretic terms. For OMQs with arbitrary ontologies and
boundedleaf CQs, NDLrewritings are constructed and evaluated in LOGCFL. We
show experimentally feasibility and scalability of our rewritings compared to
previously proposed NDLrewritings. On the negative side, we prove that
answering OMQs with treeshaped CQs is not fixedparameter tractable if the
ontology depth or the number of leaves in the CQs is regarded as the parameter,
and that answering OMQs with a fixed ontology (of infinite depth) is
NPcomplete for treeshaped and LOGCFL for boundedleaf CQs.

We present a new metric temporal logic HornMTL over dense time and its
datalog extension datalogMTL. The use of datalogMTL is demonstrated in the
context of ontologybased data access over meteorological data. We show
decidability of answering ontologymediated queries for a practically relevant
nonrecursive fragment of datalogMTL. Finally, we discuss directions of the
future work, including the potential usecases in analyzing log data of engines
and devices.

We investigate the problem whether two ALC knowledge bases are
indistinguishable by queries over a given vocabulary. We give modeltheoretic
criteria in terms of (partial) homomorphisms and products and prove that this
problem is undecidable for conjunctive queries (CQs) but 2EXPTIMEcomplete for
UCQs (unions of CQs). The same results hold if CQs are replaced by rooted CQs.
We also consider the problem whether two ALC TBoxes give the same answers to
any query in a given vocabulary over all ABoxes, and show that for CQs this
problem is undecidable, too, but becomes decidable and 2EXPTIMEcomplete in
HornALC, and even EXPTIMEcomplete in HornALC when restricted to (unions of)
rooted CQs.

We give solutions to two fundamental computational problems in ontologybased
data access with the W3C standard ontology language OWL 2 QL: the succinctness
problem for firstorder rewritings of ontologymediated queries (OMQs), and the
complexity problem for OMQ answering. We classify OMQs according to the shape
of their conjunctive queries (treewidth, the number of leaves) and the
existential depth of their ontologies. For each of these classes, we determine
the combined complexity of OMQ answering, and whether all OMQs in the class
have polynomialsize firstorder, positive existential, and nonrecursive
datalog rewritings. We obtain the succinctness results using hypergraph
programs, a new computational model for Boolean functions, which makes it
possible to connect the size of OMQ rewritings and circuit complexity.

We show that, for OWL 2 QL ontologymediated queries with (i) ontologies of
bounded depth and conjunctive queries of bounded treewidth, (ii) ontologies of
bounded depth and boundedleaf treeshaped conjunctive queries, and (iii)
arbitrary ontologies and boundedleaf treeshaped conjunctive queries, one can
construct and evaluate nonrecursive datalog rewritings by, respectively,
LOGCFL, NL and LOGCFL algorithms, which matches the optimal combined
complexity.

We design temporal description logics suitable for reasoning about temporal
conceptual data models and investigate their computational complexity. Our
formalisms are based on DLLite logics with three types of concept inclusions
(ranging from atomic concept inclusions and disjointness to the full Booleans),
as well as cardinality constraints and role inclusions. In the temporal
dimension, they capture future and past temporal operators on concepts,
flexible and rigid roles, the operators `always' and `some time' on roles, data
assertions for particular moments of time and global concept inclusions. The
logics are interpreted over the Cartesian products of object domains and the
flow of time (Z,<), satisfying the constant domain assumption. We prove that
the most expressive of our temporal description logics (which can capture
lifespan cardinalities and either qualitative or quantitative evolution
constraints) turn out to be undecidable. However, by omitting some of the
temporal operators on concepts/roles or by restricting the form of concept
inclusions we obtain logics whose complexity ranges between PSpace and
NLogSpace. These positive results were obtained by reduction to various clausal
fragments of propositional temporal logic, which opens a way to employ
propositional or firstorder temporal provers for reasoning about temporal data
models.

We investigate the size of firstorder rewritings of conjunctive queries over
OWL 2 QL ontologies of depth 1 and 2 by means of hypergraph programs computing
Boolean functions. Both positive and negative results are obtained. Conjunctive
queries over ontologies of depth 1 have polynomialsize nonrecursive datalog
rewritings; treeshaped queries have polynomial positive existential
rewritings; however, in the worst case, positive existential rewritings can
only be of superpolynomial size. Positive existential and nonrecursive datalog
rewritings of queries over ontologies of depth 2 suffer an exponential blowup
in the worst case, while firstorder rewritings are superpolynomial unless
$\text{NP} \subseteq \text{P}/\text{poly}$. We also analyse rewritings of
treeshaped queries over arbitrary ontologies and observe that the query
entailment problem for such queries is fixedparameter tractable.

The recently introduced series of description logics under the common moniker
DLLite has attracted attention of the description logic and semantic web
communities due to the low computational complexity of inference, on the one
hand, and the ability to represent conceptual modeling formalisms, on the
other. The main aim of this article is to carry out a thorough and systematic
investigation of inference in extensions of the original DLLite logics along
five axes: by (i) adding the Boolean connectives and (ii) number restrictions
to concept constructs, (iii) allowing role hierarchies, (iv) allowing role
disjointness, symmetry, asymmetry, reflexivity, irreflexivity and transitivity
constraints, and (v) adopting or dropping the unique same assumption. We
analyze the combined complexity of satisfiability for the resulting logics, as
well as the data complexity of instance checking and answering positive
existential queries. Our approach is based on embedding DLLite logics in
suitable fragments of the onevariable firstorder logic, which provides useful
insights into their properties and, in particular, computational behavior.

Our aim is to investigate ontologybased data access over temporal data with
validity time and ontologies capable of temporal conceptual modelling. To this
end, we design a temporal description logic, TQL, that extends the standard
ontology language OWL 2 QL, provides basic means for temporal conceptual
modelling and ensures firstorder rewritability of conjunctive queries for
suitably defined data instances with validity time.

We establish connections between the size of circuits and formulas computing
monotone Boolean functions and the size of firstorder and nonrecursive Datalog
rewritings for conjunctive queries over OWL 2 QL ontologies. We use known lower
bounds and separation results from circuit complexity to prove similar results
for the size of rewritings that do not use nonsignature constants. For
example, we show that, in the worst case, positive existential and nonrecursive
Datalog rewritings are exponentially longer than the original queries;
nonrecursive Datalog rewritings are in general exponentially more succinct than
positive existential rewritings; while firstorder rewritings can be
superpolynomially more succinct than positive existential rewritings.

We consider the quantifierfree languages, Bc and Bc0, obtained by augmenting
the signature of Boolean algebras with a unary predicate representing,
respectively, the property of being connected, and the property of having a
connected interior. These languages are interpreted over the regular closed
sets of ndimensional Euclidean space (n greater than 1) and, additionally,
over the regular closed polyhedral sets of ndimensional Euclidean space. The
resulting logics are examples of formalisms that have recently been proposed in
the Artificial Intelligence literature under the rubric "Qualitative Spatial
Reasoning." We prove that the satisfiability problem for Bc is undecidable over
the regular closed polyhedra in all dimensions greater than 1, and that the
satisfiability problem for both languages is undecidable over both the regular
closed sets and the regular closed polyhedra in the Euclidean plane. However,
we also prove that the satisfiability problem for Bc0 is NPcomplete over the
regular closed sets in all dimensions greater than 2, while the corresponding
problem for the regular closed polyhedra is ExpTimecomplete. Our results show,
in particular, that spatial reasoning over Euclidean spaces is much harder than
reasoning over arbitrary topological spaces.

We consider quantifierfree spatial logics, designed for qualitative spatial
representation and reasoning in AI, and extend them with the means to represent
topological connectedness of regions and restrict the number of their connected
components. We investigate the computational complexity of these logics and
show that the connectedness constraints can increase complexity from NP to
PSpace, ExpTime and, if component counting is allowed, to NExpTime.

We show that the unification problem `is there a substitution instance of a
given formula that is provable in a given logic?' is undecidable for basic
modal logics K and K4 extended with the universal modality. It follows that the
admissibility problem for inference rules is undecidable for these logics as
well. These are the first examples of standard decidable modal logics for which
the unification and admissibility problems are undecidable. We also prove
undecidability of the unification and admissibility problems for K and K4 with
at least two modal operators and nominals (instead of the universal modality),
thereby showing that these problems are undecidable for basic hybrid logics.
Recently, unification has been introduced as an important reasoning service for
description logics. The undecidability proof for K with nominals can be used to
show the undecidability of unification for boolean description logics with
nominals (such as ALCO and SHIQO). The undecidability proof for K with the
universal modality can be used to show that the unification problem relative to
role boxes is undecidable for Boolean description logic with transitive roles,
inverse roles, and role hierarchies (such as SHI and SHIQ).