
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 study the problem of learning description logic (DL) ontologies in Angluin
et al.'s framework of exact learning via queries. We admit membership queries
("is a given subsumption entailed by the target ontology?") and equivalence
queries ("is a given ontology equivalent to the target ontology?"). We present
three main results: (1) ontologies formulated in (two relevant versions of) the
description logic DLLite can be learned with polynomially many queries of
polynomial size; (2) this is not the case for ontologies formulated in the
description logic EL, even when only acyclic ontologies are admitted; and (3)
ontologies formulated in a fragment of EL related to the web ontology language
OWL 2 RL can be learned in polynomial time. We also show that neither
membership nor equivalence queries alone are sufficient in cases (1) and (3).

In 1930s Paul Erdos conjectured that for any positive integer $C$ in any
infinite $\pm 1$ sequence $(x_n)$ there exists a subsequence $x_d, x_{2d},
x_{3d},\dots, x_{kd}$, for some positive integers $k$ and $d$, such that $\mid
\sum_{i=1}^k x_{i\cdot d} \mid >C$. The conjecture has been referred to as one
of the major open problems in combinatorial number theory and discrepancy
theory. For the particular case of $C=1$ a human proof of the conjecture
exists; for $C=2$ a bespoke computer program had generated sequences of length
$1124$ of discrepancy $2$, but the status of the conjecture remained open even
for such a small bound. We show that by encoding the problem into Boolean
satisfiability and applying the state of the art SAT solvers, one can obtain a
discrepancy $2$ sequence of length $1160$ and a proof of the Erd\H{o}s
discrepancy conjecture for $C=2$, claiming that no discrepancy 2 sequence of
length $1161$, or more, exists. In the similar way, we obtain a precise bound
of $127\,645$ on the maximal lengths of both multiplicative and completely
multiplicative sequences of discrepancy $3$. We also demonstrate that
unrestricted discrepancy 3 sequences can be longer than $130\,000$.

In 1930s Paul Erdos conjectured that for any positive integer C in any
infinite +1 1 sequence (x_n) there exists a subsequence x_d, x_{2d}, ... ,
x_{kd} for some positive integers k and d, such that x_d + x_{2d} + ... +
x_{kd}> C. The conjecture has been referred to as one of the major open
problems in combinatorial number theory and discrepancy theory. For the
particular case of C=1 a human proof of the conjecture exists; for C=2 a
bespoke computer program had generated sequences of length 1124 having
discrepancy 2, but the status of the conjecture remained open even for such a
small bound. We show that by encoding the problem into Boolean satisfiability
and applying the state of the art SAT solvers, one can obtain a sequence of
length 1160 with discrepancy 2 and a proof of the Erdos discrepancy conjecture
for C=2, claiming that no sequence of length 1161 and discrepancy 2 exists. We
also present our partial results for the case of C=3.

We study a logicbased approach to versioning of ontologies. Under this view,
ontologies provide answers to queries about some vocabulary of interest. The
difference between two versions of an ontology is given by the set of queries
that receive different answers. We investigate this approach for terminologies
given in the description logic EL extended with role inclusions and domain and
range restrictions for three distinct types of queries: subsumption, instance,
and conjunctive queries. In all three cases, we present polynomialtime
algorithms that decide whether two terminologies give the same answers to
queries over a given vocabulary and compute a succinct representation of the
difference if it is non empty. We present an implementation, CEX2, of the
developed algorithms for subsumption and instance queries and apply it to
distinct versions of Snomed CT and the NCI ontology.

In this paper we consider the specification and verification of
infinitestate systems using temporal logic. In particular, we describe
parameterised systems using a new variety of firstorder temporal logic that is
both powerful enough for this form of specification and tractable enough for
practical deductive verification. Importantly, the power of the temporal
language allows us to describe (and verify) asynchronous systems, communication
delays and more complex properties such as liveness and fairness properties.
These aspects appear difficult for many other approaches to infinitestate
verification.

Until recently, FirstOrder Temporal Logic (FOTL) has been little understood.
While it is well known that the full logic has no finite axiomatisation, a more
detailed analysis of fragments of the logic was not previously available.
However, a breakthrough by Hodkinson et.al., identifying a finitely
axiomatisable fragment, termed the monodic fragment, has led to improved
understanding of FOTL. Yet, in order to utilise these theoretical advances, it
is important to have appropriate proof techniques for the monodic fragment.
In this paper, we modify and extend the clausal temporal resolution
technique, originally developed for propositional temporal logics, to enable
its use in such monodic fragments. We develop a specific normal form for
formulae in FOTL, and provide a complete resolution calculus for formulae in
this form. Not only is this clausal resolution technique useful as a practical
proof technique for certain monodic classes, but the use of this approach
provides us with increased understanding of the monodic fragment. In
particular, we here show how several features of monodic FOTL are established
as corollaries of the completeness result for the clausal temporal resolution
method. These include definitions of new decidable monodic classes,
simplification of existing monodic classes by reductions, and completeness of
clausal temporal resolution in the case of monodic logics with expanding
domains, a case with much significance in both theory and practice.