
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.

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 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.

In the propositional modal (and algebraic) treatment of twovariable
firstorder logic equality is modelled by a `diagonal' constant, interpreted in
square products of universal frames as the identity (also known as the
`diagonal') relation. Here we study the decision problem of products of two
arbitrary modal logics equipped with such a diagonal. As the presence or
absence of equality in twovariable firstorder logic does not influence the
complexity of its satisfiability problem, one might expect that adding a
diagonal to product logics in general is similarly harmless. We show that this
is far from being the case, and there can be quite a big jump in complexity,
even from decidable to the highly undecidable. Our undecidable logics can also
be viewed as new fragments of first order logic where adding equality changes
a decidable fragment to undecidable. We prove our results by a novel
application of counter machine problems. While our formalism apparently cannot
force reliable counter machine computations directly, the presence of a unique
diagonal in the models makes it possible to encode both lossy and
insertionerror computations, for the same sequence of instructions. We show
that, given such a pair of faulty computations, it is then possible to
reconstruct a reliable run from them.

This paper investigates the impact of query topology on the difficulty of
answering conjunctive queries in the presence of OWL 2 QL ontologies. Our first
contribution is to clarify the worstcase size of positive existential (PE),
nonrecursive Datalog (NDL), and firstorder (FO) rewritings for various
classes of treelike conjunctive queries, ranging from linear queries to
bounded treewidth queries. Perhaps our most surprising result is a
superpolynomial lower bound on the size of PErewritings that holds already for
linear queries and ontologies of depth 2. More positively, we show that
polynomialsize NDLrewritings always exist for treeshaped queries with a
bounded number of leaves (and arbitrary ontologies), and for bounded treewidth
queries paired with bounded depth ontologies. For FOrewritings, we equate the
existence of polysize rewritings with wellknown problems in Boolean circuit
complexity. As our second contribution, we analyze the computational complexity
of query answering and establish tractability results (either NL or
LOGCFLcompleteness) for a range of queryontology pairs. Combining our new
results with those from the literature yields a complete picture of the
succinctness and complexity landscapes for the considered classes of queries
and ontologies.

In this paper we consider the normal modal logics of elementary classes
defined by firstorder formulas of the form $\forall x_0 \exists x_1 \dots
\exists x_n \bigwedge x_i R_\lambda x_j$. We prove that many properties of
these logics, such as finite axiomatisability, elementarity, axiomatisability
by a set of canonical formulas or by a single generalised Sahlqvist formula,
together with modal definability of the initial formula, either simultaneously
hold or simultaneously do not hold.

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.

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.

Sahlqvist formulas are a syntactically specified class of modal formulas
proposed by Hendrik Sahlqvist in 1975. They are important because of their
firstorder definability and canonicity, and hence axiomatize complete modal
logics. The firstorder properties definable by Sahlqvist formulas were
syntactically characterized by Marcus Kracht in 1993. The present paper extends
Kracht's theorem to the class of `generalized Sahlqvist formulas' introduced by
Goranko and Vakarelov and describes an appropriate generalization of Kracht
formulas.