Unification in Description Logics has been introduced as a means to detect
redundancies in ontologies. We try to extend the known decidability results for
unification in the Description Logic $\mathcal{EL}$ to disunification since
negative constraints can be used to avoid unwanted unifiers. While decidability
of the solvability of general $\mathcal{EL}$-disunification problems remains an
open problem, we obtain NP-completeness results for two interesting special
cases: dismatching problems, where one side of each negative constraint must be
ground, and local solvability of disunification problems, where we consider
only solutions that are constructed from terms occurring in the input problem.
More precisely, we first show that dismatching can be reduced to local
disunification, and then provide two complementary NP-algorithms for finding
local solutions of disunification problems.
Spatial aspects of computation are becoming increasingly relevant in Computer
Science, especially in the field of collective adaptive systems and when
dealing with systems distributed in physical space. Traditional formal
verification techniques are well suited to analyse the temporal evolution of
programs; however, properties of space are typically not taken into account
explicitly. We present a topology-based approach to formal verification of
spatial properties depending upon physical space. We define an appropriate
logic, stemming from the tradition of topological interpretations of modal
logics, dating back to earlier logicians such as Tarski, where modalities
describe neighbourhood. We lift the topological definitions to the more general
setting of closure spaces, also encompassing discrete, graph-based structures.
We extend the framework with a spatial surrounded operator, a propagation
operator and with some collective operators. The latter are interpreted over
arbitrary sets of points instead of individual points in space. We define
efficient model checking procedures, both for the individual and the collective
spatial fragments of the logic and provide a proof-of-concept tool.
When given a class of functions and a finite collection of sets, one might be
interested whether the class in question contains any function whose domain is
a subset of the union of the sets of the given collection and whose
restrictions to all of them belong to this class. The collections with the
formulated property are said to be strongly join permitting for the given class
(the notion of join permitting collection is defined in the same way, but
without the words "a subset of"). Three theorems concerning certain instances
of the problem are proved. A necessary and sufficient condition for being
strongly join permitting is given for the case when, for some $n$, the class
consists of the potentially partial recursive functions of $n$ variables, and
the collection consists of sets of $n$-tuples of natural numbers. The second
theorem gives a sufficient condition for the case when the class consists of
the continuous partial functions between two given topological spaces, and the
collection consists of subsets of the first of them (the condition is also
necessary under a weak assumption on the second one). The third theorem is of a
similar character but, instead of continuity, it concerns computability in the
spirit of the one in effective topological spaces.
We study a fine hierarchy of Borel-piecewise continuous functions,
especially, between closed-piecewise continuity and $G_\delta$-piecewise
continuity. Our aim is to understand how a priority argument in computability
theory is connected to the notion of $G_\delta$-piecewise continuity, and then
we utilize this connection to obtain separation results on subclasses of
$G_\delta$-piecewise continuous reductions for uniformization problems on
set-valued functions with compact graphs. This method is also applicable for
separating various non-constructive principles in the Weihrauch lattice.
In the design of software and cyber-physical systems, security is often
perceived as a qualitative need, but can only be attained quantitatively.
Especially when distributed components are involved, it is hard to predict and
confront all possible attacks. A main challenge in the development of complex
systems is therefore to discover attacks, quantify them to comprehend their
likelihood, and communicate them to non-experts for facilitating the decision
process. To address this three-sided challenge we propose a protection analysis
over the Quality Calculus that (i) computes all the sets of data required by an
attacker to reach a given location in a system, (ii) determines the cheapest
set of such attacks for a given notion of cost, and (iii) derives an attack
tree that displays the attacks graphically. The protection analysis is first
developed in a qualitative setting, and then extended to quantitative settings
following an approach applicable to a great many contexts. The quantitative
formulation is implemented as an optimisation problem encoded into
Satisfiability Modulo Theories, allowing us to deal with complex cost
structures. The usefulness of the framework is demonstrated on a national-scale
authentication system, studied through a Java implementation of the framework.
An approach to the formal description of service contracts is presented in
terms of automata. We focus on the basic property of guaranteeing that in the
multi-party composition of principals each of them gets his requests satisfied,
so that the overall composition reaches its goal. Depending on whether requests
are satisfied synchronously or asynchronously, we construct an orchestrator
that at static time either yields composed services enjoying the required
properties or detects the principals responsible for possible violations. To do
that in the asynchronous case we resort to Linear Programming techniques. We
also relate our automata with two logically based methods for specifying
contracts.
We propose a type system for a calculus of contracting processes. Processes
can establish sessions by stipulating contracts, and then can interact either
by keeping the promises made, or not. Type safety guarantees that a typeable
process is honest - that is, it abides by the contracts it has stipulated in
all possible contexts, even in presence of dishonest adversaries. Type
inference is decidable, and it allows to safely approximate the honesty of
processes using either synchronous or asynchronous communication.
We study Gaifman locality and Hanf locality of an extension of first-order
logic with modulo p counting quantifiers (FO+MOD_p, for short) with arbitrary
numerical predicates. We require that the validity of formulas is independent
of the particular interpretation of the numerical predicates and refer to such
formulas as arb-invariant formulas. This paper gives a detailed picture of
locality and non-locality properties of arb-invariant FO+MOD_p. For example, on
the class of all finite structures, for any p >= 2, arb-invariant FO+MOD_p is
neither Hanf nor Gaifman local with respect to a sublinear locality radius.
However, in case that p is an odd prime power, it is weakly Gaifman local with
a polylogarithmic locality radius. And when restricting attention to the class
of string structures, for odd prime powers p, arb-invariant FO+MOD_p is both
Hanf and Gaifman local with a polylogarithmic locality radius. Our negative
results build on examples of order-invariant FO+MOD_p formulas presented in
Niemistö's PhD thesis. Our positive results make use of the close connection
between FO+MOD_p and Boolean circuits built from NOT-gates and AND-, OR-, and
MOD_p- gates of arbitrary fan-in.
Linear rules have played an increasing role in structural proof theory in
recent years. It has been observed that the set of all sound linear inference
rules in Boolean logic is already coNP-complete, i.e. that every Boolean
tautology can be written as a (left- and right-)linear rewrite rule. In this
paper we study properties of systems consisting only of linear inferences. Our
main result is that the length of any 'nontrivial' derivation in such a system
is bound by a polynomial. As a consequence there is no polynomial-time
decidable sound and complete system of linear inferences, unless coNP=NP. We
draw tools and concepts from term rewriting, Boolean function theory and graph
theory in order to access some required intermediate results. At the same time
we make several connections between these areas that, to our knowledge, have
not yet been presented and constitute a rich theoretical framework for
reasoning about linear TRSs for Boolean logic.
We use modal logic as a framework for coalgebraic trace semantics, and show
the flexibility of the approach with concrete examples such as the language
semantics of weighted, alternating and tree automata, and the trace semantics
of generative probabilistic systems. We provide a sufficient condition under
which a logical semantics coincides with the trace semantics obtained via a
given determinization construction. Finally, we consider a condition that
guarantees the existence of a canonical determinization procedure that is
correct with respect to a given logical semantics. That procedure is closely
related to Brzozowski's minimization algorithm.
We stratify intuitionistic first-order logic over $(\forall,\to)$ into
fragments determined by the alternation of positive and negative occurrences of
quantifiers (Mints hierarchy).
We study the decidability and complexity of these fragments. We prove that
even the $\Delta_2$ level is undecidable and that $\Sigma_1$ is
Expspace-complete. We also prove that the arity-bounded fragment of $\Sigma_1$
is complete for co-Nexptime.
We study which standard operators of probabilistic process calculi allow for
compositional reasoning with respect to bisimulation metric semantics. We argue
that uniform continuity (generalizing the earlier proposed property of
non-expansiveness) captures the essential nature of compositional reasoning and
allows now also to reason compositionally about recursive processes. We
characterize the distance between probabilistic processes composed by standard
process algebra operators. Combining these results, we demonstrate how
compositional reasoning about systems specified by continuous process algebra
operators allows for metric assume-guarantee like performance validation.
Many automatic theorem provers are restricted to untyped logics, and existing
translations from typed logics are bulky or unsound. Recent research proposes
monotonicity as a means to remove some clutter when translating monomorphic to
untyped first-order logic. Here we pursue this approach systematically,
analysing formally a variety of encodings that further improve on efficiency
while retaining soundness and completeness. We extend the approach to rank-1
polymorphism and present alternative schemes that lighten the translation of
polymorphic symbols based on the novel notion of "cover". The new encodings are
implemented in Isabelle/HOL as part of the Sledgehammer tool. We include
informal proofs of soundness and correctness, and have formalised the
monomorphic part of this work in Isabelle/HOL. Our evaluation finds the new
encodings vastly superior to previous schemes.
