Publications

This paper presents an up-to-date and refined version of the SCL calculus for
first-order logic without equality. The refinement mainly consists of the
following two parts: First, we incorporate a stronger notion of regularity into
SCL(FOL). Our regularity definition is adapted from the SCL(T) calculus. This
adapted definition guarantees non-redundant clause learning during a run of
SCL. However, in contrast to the original presentation, it does not require
exhaustive propagation. Second, we introduce trail and model bounding to
achieve termination guarantees. In previous versions, no termination guarantees
about SCL were achieved. Last, we give rigorous proofs for soundness,
completeness and clause learning guarantees of SCL(FOL) and put SCL(FOL) into
context of existing first-order calculi.

Clause sets saturated by hierarchic superposition do not offer an explicit
model representation, rather the guarantee that all non-redundant inferences
have been performed without deriving a contradiction. We present an approach to
explicit model construction for saturated constrained Horn clauses. Constraints
are in linear arithmetic, the first-order part is restricted to a function-free
language. The model construction is effective and clauses can be evaluated with
respect to the model. Furthermore, we prove that our model construction
produces the least model.

In a previous paper, we have shown that clause sets belonging to the Horn
Bernays-Sch\"onfinkel fragment over simple linear real arithmetic (HBS(SLR))
can be translated into HBS clause sets over a finite set of first-order
constants. The translation preserves validity and satisfiability and it is
still applicable if we extend our input with positive universally or
existentially quantified verification conditions (conjectures). We call this
translation a Datalog hammer. The combination of its implementation in
SPASS-SPL with the Datalog reasoner VLog establishes an effective way of
deciding verification conditions in the Horn fragment. We verify supervisor
code for two examples: a lane change assistant in a car and an electronic
control unit of a supercharged combustion engine. In this paper, we improve our
Datalog hammer in several ways: we generalize it to mixed real-integer
arithmetic and finite first-order sorts; we extend the class of acceptable
inequalities beyond variable bounds and positively grounded inequalities; and
we significantly reduce the size of the hammer output by a soft typing
discipline. We call the result the sorted Datalog hammer. It not only allows us
to handle more complex supervisor code and to model already considered
supervisor code more concisely, but it also improves our performance on real
world benchmark examples. Finally, we replace the before file-based interface
between SPASS-SPL and VLog by a close coupling resulting in a single executable
binary.

Abduction in description logics finds extensions of a knowledge base to make
it entail an observation. As such, it can be used to explain why the
observation does not follow, to repair incomplete knowledge bases, and to
provide possible explanations for unexpected observations. We consider TBox
abduction in the lightweight description logic EL, where the observation is a
concept inclusion and the background knowledge is a TBox, i.e., a set of
concept inclusions. To avoid useless answers, such problems usually come with
further restrictions on the solution space and/or minimality criteria that help
sort the chaff from the grain. We argue that existing minimality notions are
insufficient, and introduce connection minimality. This criterion follows
Occam's razor by rejecting hypotheses that use concept inclusions unrelated to
the problem at hand. We show how to compute a special class of
connection-minimal hypotheses in a sound and complete way. Our technique is
based on a translation to first-order logic, and constructs hypotheses based on
prime implicates. We evaluate a prototype implementation of our approach on
ontologies from the medical domain.

We propose a new calculus SCL(EQ) for first-order logic with equality that
only learns non-redundant clauses. Following the idea of CDCL (Conflict Driven
Clause Learning) and SCL (Clause Learning from Simple Models) a ground literal
model assumption is used to guide inferences that are then guaranteed to be
non-redundant. Redundancy is defined with respect to a dynamically changing
ordering derived from the ground literal model assumption. We prove SCL(EQ)
sound and complete and provide examples where our calculus improves on
superposition.

Recently, symbolic computation and computer algebra systems have been
successfully applied in systems biology, especially in chemical reaction
network theory. One advantage of symbolic computation is its potential for
qualitative answers to biological questions. Qualitative methods analyze
dynamical input systems as formal objects, in contrast to investigating only
part of the state space, as is the case with numerical simulation. However,
symbolic computation tools and libraries have a different set of requirements
for their input data than their numerical counterparts. A common format used in
mathematical modeling of biological processes is SBML. We illustrate that the
use of SBML data in symbolic computation requires significant pre-processing,
incorporating external biological and mathematical expertise. ODEbase provides
high quality symbolic computation input data derived from established existing
biomodels, covering in particular the BioModels database.

We designed a superposition calculus for a clausal fragment of extensional
polymorphic higher-order logic that includes anonymous functions but excludes
Booleans. The inference rules work on $\beta\eta$-equivalence classes of
$\lambda$-terms and rely on higher-order unification to achieve refutational
completeness. We implemented the calculus in the Zipperposition prover and
evaluated it on TPTP and Isabelle benchmarks. The results suggest that
superposition is a suitable basis for higher-order reasoning.

The Bernays-Sch\"onfinkel first-order logic fragment over simple linear real
arithmetic constraints BS(SLR) is known to be decidable. We prove that BS(SLR)
clause sets with both universally and existentially quantified verification
conditions (conjectures) can be translated into BS(SLR) clause sets over a
finite set of first-order constants. For the Horn case, we provide a Datalog
hammer preserving validity and satisfiability. A toolchain from the BS(LRA)
prover SPASS-SPL to the Datalog reasoner VLog establishes an effective way of
deciding verification conditions in the Horn fragment. This is exemplified by
the verification of supervisor code for a lane change assistant in a car and of
an electronic control unit for a supercharged combustion engine.

We study real steady state varieties of the dynamics of chemical reaction
networks. The dynamics are derived using mass action kinetics with parametric
reaction rates. The models studied are not inherently parametric in nature.
Rather, our interest in parameters is motivated by parameter uncertainty, as
reaction rates are typically either measured with limited precision or
estimated. We aim at detecting toricity and shifted toricity, using a framework
that has been recently introduced and studied for the non-parametric case over
both the real and the complex numbers. While toricity requires that the variety
specifies a subgroup of the direct power of the multiplicative group of the
underlying field, shifted toricity requires only a coset. In the non-parametric
case these requirements establish real decision problems. In the presence of
parameters we must go further and derive necessary and sufficient conditions in
the parameters for toricity or shifted toricity to hold. Technically, we use
real quantifier elimination methods. Our computations on biological networks
here once more confirm shifted toricity as a relevant concept, while toricity
holds only for degenerate parameter choices.

We consider the problem of binomiality of the steady state ideals of
biochemical reaction networks. We are interested in finding polynomial
conditions on the parameters such that the steady state ideal of a chemical
reaction network is binomial under every specialisation of the parameters if
the conditions on the parameters hold. We approach the binomiality problem
using Comprehensive Gr\"obner systems. Considering rate constants as
parameters, we compute comprehensive Gr\"obner systems for various reactions.
In particular, we make automatic computations on n-site phosphorylations and
biomodels from the Biomodels repository using the grobcov library of the
computer algebra system Singular.

We introduce refutationally complete superposition calculi for intentional
and extensional clausal $\lambda$-free higher-order logic, two formalisms that
allow partial application and applied variables. The calculi are parameterized
by a term order that need not be fully monotonic, making it possible to employ
the $\lambda$-free higher-order lexicographic path and Knuth-Bendix orders. We
implemented the calculi in the Zipperposition prover and evaluated them on
Isabelle/HOL and TPTP benchmarks. They appear promising as a stepping stone
towards complete, highly efficient automatic theorem provers for full
higher-order logic.

We lift the SCL calculus for first-order logic without equality to the SCL(T)
calculus for first-order logic without equality modulo a background theory. In
a nutshell, the SCL(T) calculus describes a new way to guide hierarchic
resolution inferences by a partial model assumption instead of an a priori
fixed order as done for instance in hierarchic superposition. The model
representation consists of ground background theory literals and ground
foreground first-order literals. One major advantage of the model guided
approach is that clauses generated by SCL(T) enjoy a non-redundancy property
that makes expensive testing for tautologies and forward subsumption completely
obsolete. SCL(T) is a semi-decision procedure for pure clause sets that are
clause sets without first-order function symbols ranging into the background
theory sorts. Moreover, SCL(T) can be turned into a decision procedure if the
considered combination of a first-order logic modulo a background theory enjoys
an abstract finite model property.

I develop a formal framework for propositional satifisfiability with the conflict-driven clause learning (CDCL) procedure using the Isabelle/HOL proof assistant. The framework offers a convenient way to prove metatheorems and experiment with variants, including the Davis-Putnam-Logemann-Loveland procedure. The most noteworthy aspects of my work are the inclusion of rules for forget and restart and the refinement approach. I use the formalization to develop three extensions: First, an incremental solving extension of CDCL. Second, I verify an optimizing CDCL (OCDCL): Given a cost function on literals, OCDCL derives an optimal model with minimum cost. Finally, I work on model covering. Thanks to the CDCL framework I can reuse, these extensions are easier to develop. Through a chain of refinements, I connect the abstract CDCL calculus first to a more concrete calculus, then to a SAT solver expressed in a simple functional programming language, and finally to a SAT solver in an imperative language, with total correctness guarantees. The imperative version relies on the two-watched-literal data structure and other optimizations found in modern solvers. I used the Isabelle Refinement Framework to automate the most tedious refinement steps. After that, I extend this work with further optimizations like blocking literals and the use of machine words as long as possible, before switching to unbounded integers to keep completeness.

Loop acceleration can be used to prove safety, reachability, runtime bounds,
and (non-)termination of programs operating on integers. To this end, a variety
of acceleration techniques has been proposed. However, all of them are
monolithic: Either they accelerate a loop successfully or they fail completely.
In contrast, we present a calculus that allows for combining acceleration
techniques in a modular way and we show how to integrate many existing
acceleration techniques into our calculus. Moreover, we propose two novel
acceleration techniques that can be incorporated into our calculus seamlessly.
An empirical evaluation demonstrates the applicability of our approach.

We present a symbolic algorithmic approach that allows to compute invariant
manifolds and corresponding reduced systems for differential equations modeling
biological networks which comprise chemical reaction networks for cellular
biochemistry, and compartmental models for pharmacology, epidemiology and
ecology. Multiple time scales of a given network are obtained by scaling, based
on tropical geometry. Our reduction is mathematically justified within a
singular perturbation setting using a recent result by Cardin and Teixeira. The
existence of invariant manifolds is subject to hyperbolicity conditions, which
we test algorithmically using Hurwitz criteria. We finally obtain a sequence of
nested invariant manifolds and respective reduced systems on those manifolds.
Our theoretical results are generally accompanied by rigorous algorithmic
descriptions suitable for direct implementation based on existing off-the-shelf
software systems, specifically symbolic computation libraries and
Satisfiability Modulo Theories solvers. We present computational examples taken
from the well-known BioModels database using our own prototypical
implementations.

We study binomiality of the steady state ideals of chemical reaction
networks. Considering rate constants as indeterminates, the concept of
unconditional binomiality has been introduced and an algorithm based on linear
algebra has been proposed in a recent work for reversible chemical reaction
networks, which has a polynomial time complexity upper bound on the number of
species and reactions. In this article, using a modified version of
species--reaction graphs, we present an algorithm based on graph theory which
performs by adding and deleting edges and changing the labels of the edges in
order to test unconditional binomiality. We have implemented our graph
theoretical algorithm as well as the linear algebra one in Maple and made
experiments on biochemical models. Our experiments show that the performance of
the graph theoretical approach is similar to or better than the linear algebra
approach, while it is drastically faster than Groebner basis and quantifier
elimination methods.

Motivated by problems arising with the symbolic analysis of steady state
ideals in Chemical Reaction Network Theory, we consider the problem of testing
whether the points in a complex or real variety with non-zero coordinates form
a coset of a multiplicative group. That property corresponds to Shifted
Toricity, a recent generalization of toricity of the corresponding polynomial
ideal. The key idea is to take a geometric view on varieties rather than an
algebraic view on ideals. Recently, corresponding coset tests have been
proposed for complex and for real varieties. The former combine numerous
techniques from commutative algorithmic algebra with Gr\"obner bases as the
central algorithmic tool. The latter are based on interpreted first-order logic
in real closed fields with real quantifier elimination techniques on the
algorithmic side. Here we take a new logic approach to both theories, complex
and real, and beyond. Besides alternative algorithms, our approach provides a
unified view on theories of fields and helps to understand the relevance and
interconnection of the rich existing literature in the area, which has been
focusing on complex numbers, while from a scientific point of view the
(positive) real numbers are clearly the relevant domain in chemical reaction
network theory. We apply prototypical implementations of our new approach to a
set of 129 models from the BioModels repository.

We discuss the effective computation of geometric singularities of implicit
ordinary differential equations over the real numbers using methods from logic.
Via the Vessiot theory of differential equations, geometric singularities can
be characterised as points where the behaviour of a certain linear system of
equations changes. These points can be discovered using a specifically adapted
parametric generalisation of Gaussian elimination combined with heuristic
simplification techniques and real quantifier elimination methods. We
demonstrate the relevance and applicability of our approach with computational
experiments using a prototypical implementation in Reduce.

Many applications of automated deduction require reasoning in first-order
logic modulo background theories, in particular some form of integer
arithmetic. A major unsolved research challenge is to design theorem provers
that are "reasonably complete" even in the presence of free function symbols
ranging into a background theory sort. The hierarchic superposition calculus of
Bachmair, Ganzinger, and Waldmann already supports such symbols, but, as we
demonstrate, not optimally. This paper aims to rectify the situation by
introducing a novel form of clause abstraction, a core component in the
hierarchic superposition calculus for transforming clauses into a form needed
for internal operation. We argue for the benefits of the resulting calculus and
provide two new completeness results: one for the fragment where all
background-sorted terms are ground and another one for a special case of linear
(integer or rational) arithmetic as a background theory.

We consider a problem from biological network analysis of determining regions
in a parameter space over which there are multiple steady states for positive
real values of variables and parameters. We describe multiple approaches to
address the problem using tools from Symbolic Computation. We describe how
progress was made to achieve semi-algebraic descriptions of the
multistationarity regions of parameter space, and compare symbolic results to
numerical methods. The biological networks studied are models of the
mitogen-activated protein kinases (MAPK) network which has already consumed
considerable effort using special insights into its structure of corresponding
models. Our main example is a model with 11 equations in 11 variables and 19
parameters, 3 of which are of interest for symbolic treatment. The model also
imposes positivity conditions on all variables and parameters.
We apply combinations of symbolic computation methods designed for mixed
equality/inequality systems, specifically virtual substitution, lazy real
triangularization and cylindrical algebraic decomposition, as well as a
simplification technique adapted from Gaussian elimination and graph theory. We
are able to determine multistationarity of our main example over a
2-dimensional parameter space. We also study a second MAPK model and a symbolic
grid sampling technique which can locate such regions in 3-dimensional
parameter space.

Automated theorem provers are now commonly used within interactive theorem
provers to discharge an increasingly large number of proof obligations. To
maintain the trustworthiness of a proof, the automatically found proof must be
verified inside the proof assistant. We present here a reconstruction procedure
in the proof assistant Isabelle/HOL for proofs generated by the satisfiability
modulo theories solver veriT which is part of the smt tactic. We describe in
detail the architecture of our improved reconstruction method and the
challenges we faced in designing it. Our experiments show that the
veriT-powered smt tactic is regularly suggested by Sledgehammer as the fastest
method to automatically solve proof goals.

We present a technique to infer lower bounds on the worst-case runtime
complexity of integer programs, where in contrast to earlier work, our approach
is not restricted to tail-recursion. Our technique constructs symbolic
representations of program executions using a framework for iterative,
under-approximating program simplification. The core of this simplification is
a method for (under-approximating) program acceleration based on recurrence
solving and a variation of ranking functions. Afterwards, we deduce asymptotic
lower bounds from the resulting simplified programs using a special-purpose
calculus and an SMT encoding. We implemented our technique in our tool LoAT and
show that it infers non-trivial lower bounds for a large class of examples.

We present the first approach to prove non-termination of integer programs
that is based on loop acceleration. If our technique cannot show
non-termination of a loop, it tries to accelerate it instead in order to find
paths to other non-terminating loops automatically. The prerequisites for our
novel loop acceleration technique generalize a simple yet effective
non-termination criterion. Thus, we can use the same program transformations to
facilitate both non-termination proving and loop acceleration. In particular,
we present a novel invariant inference technique that is tailored to our
approach. An extensive evaluation of our fully automated tool LoAT shows that
it is competitive with the state of the art.

We consider the termination problem for triangular weakly non-linear loops
(twn-loops) over some ring $\mathcal{S}$ like $\mathbb{Z}$, $\mathbb{Q}$, or
$\mathbb{R}$. Essentially, the guard of such a loop is an arbitrary Boolean
formula over (possibly non-linear) polynomial inequations, and the body is a
single assignment $(x_1, \ldots, x_d) \longleftarrow (c_1 \cdot x_1 + p_1,
\ldots, c_d \cdot x_d + p_d)$ where each $x_i$ is a variable, $c_i \in
\mathcal{S}$, and each $p_i$ is a (possibly non-linear) polynomial over
$\mathcal{S}$ and the variables $x_{i+1},\ldots,x_{d}$. We present a reduction
from the question of termination to the existential fragment of the first-order
theory of $\mathcal{S}$ and $\mathbb{R}$. For loops over $\mathbb{R}$, our
reduction entails decidability of termination. For loops over $\mathbb{Z}$ and
$\mathbb{Q}$, it proves semi-decidability of non-termination.
Furthermore, we present a transformation to convert certain non-twn-loops
into twn-form. Then the original loop terminates iff the transformed loop
terminates over a specific subset of $\mathbb{R}$, which can also be checked
via our reduction. This transformation also allows us to prove tight complexity
bounds for the termination problem for two important classes of loops which can
always be transformed into twn-loops.

We consider the problem whether termination of affine integer loops is
decidable. Since Tiwari conjectured decidability in 2004, only special cases
have been solved. We complement this work by proving decidability for the case
that the update matrix is triangular.

We consider the problem of testing whether the points in a complex or real
variety with non-zero coordinates form a multiplicative group or, more
generally, a coset of a multiplicative group. For the coset case, we study the
notion of shifted toric varieties which generalizes the notion of toric
varieties. This requires a geometric view on the varieties rather than an
algebraic view on the ideals. We present algorithms and computations on 129
models from the BioModels repository testing for group and coset structures
over both the complex numbers and the real numbers. Our methods over the
complex numbers are based on Gr\"obner basis techniques and binomiality tests.
Over the real numbers we use first-order characterizations and employ real
quantifier elimination. In combination with suitable prime decompositions and
restrictions to subspaces it turns out that almost all models show coset
structure. Beyond our practical computations, we give upper bounds on the
asymptotic worst-case complexity of the corresponding problems by proposing
single exponential algorithms that test complex or real varieties for toricity
or shifted toricity. In the positive case, these algorithms produce generating
binomials. In addition, we propose an asymptotically fast algorithm for testing
membership in a binomial variety over the algebraic closure of the rational
numbers.

A number of first-order calculi employ an explicit model representation
formalism for automated reasoning and for detecting satisfiability. Many of
these formalisms can represent infinite Herbrand models. The first-order
fragment of monadic, shallow, linear, Horn (MSLH) clauses, is such a formalism
used in the approximation refinement calculus. Our first result is a finite
model property for MSLH clause sets. Therefore, MSLH clause sets cannot
represent models of clause sets with inherently infinite models. Through a
translation to tree automata, we further show that this limitation also applies
to the linear fragments of implicit generalizations, which is the formalism
used in the model-evolution calculus, to atoms with disequality constraints,
the formalisms used in the non-redundant clause learning calculus (NRCL), and
to atoms with membership constraints, a formalism used for example in decision
procedures for algebraic data types. Although these formalisms cannot represent
models of clause sets with inherently infinite models, through an additional
approximation step they can. This is our second main result. For clause sets
including the definition of an equivalence relation with the help of an
additional, novel approximation, called reflexive relation splitting, the
approximation refinement calculus can automatically show satisfiability through
the MSLH clause set formalism.

First-order logic is one of the most prominent formalisms in computer science and mathematics. Since there is no algorithm capable of solving its satisfiability problem, first-order logic is said to be undecidable. The classical decision problem is the quest for a delineation between the decidable and the undecidable parts. The results presented in this thesis shed more light on the boundary and open new perspectives on the landscape of known decidable fragments. In the first part we focus on the new concept of separateness of variables and explore its applicability to the classical decision problem and beyond. Two disjoint sets of first-order variables are separated in a given formula if none of its atoms contains variables from both sets. This notion facilitates the definition of decidable extensions of many well-known decidable first-order fragments. We demonstrate this for several prefix fragments, several guarded fragments, the two-variable fragment, and for the fluted fragment. Although the extensions exhibit the same expressive power as the respective originals, certain logical properties can be expressed much more succinctly. In two cases the succinctness gap cannot be bounded using elementary functions. This fact already hints at computationally hard satisfiability problems. Indeed, we derive non-elementary lower bounds for the separated fragment, an extension of the Bernays-Schönfinkel-Ramsey fragment (E*A*-prefix sentences). On the semantic level, separateness of quantified variables may lead to weaker dependences than we encounter in general. We investigate this property in the context of model-checking games. The focus of the second part of the thesis is on linear arithmetic with uninterpreted predicates. Two novel decidable fragments are presented, both based on the Bernays-Schönfinkel-Ramsey fragment. On the negative side, we identify several small fragments of the language for which satisfiability is undecidable.

The classical decision problem, as it is understood today, is the quest for a
delineation between the decidable and the undecidable parts of first-order
logic based on elegant syntactic criteria. In this paper, we treat the concept
of separateness of variables and explore its applicability to the classical
decision problem. Two disjoint sets of first-order variables are separated in a
given formula if variables from the two sets never co-occur in any atom of that
formula. This simple notion facilitates extending many well-known decidable
first-order fragments significantly and in a way that preserves decidability.
We will demonstrate that for several prefix fragments, several guarded
fragments, the two-variable fragment, and for the fluted fragment. Altogether,
we will investigate nine such extensions more closely. Interestingly, each of
them contains the relational monadic first-order fragment without equality.
Although the extensions exhibit the same expressive power as the respective
originals, certain logical properties can be expressed much more succinctly. In
three cases the succinctness gap cannot be bounded using any elementary
function.

While syntactic inference restrictions don't play an important role for SAT,
they are an essential reasoning technique for more expressive logics, such as
first-order logic, or fragments thereof. In particular, they can result in
short proofs or model representations. On the other hand, semantically guided
inference systems enjoy important properties, such as the generation of solely
non-redundant clauses. I discuss to what extend the two paradigms may be
unifiable.

We consider systems of strict multivariate polynomial inequalities over the
reals. All polynomial coefficients are parameters ranging over the reals, where
for each coefficient we prescribe its sign. We are interested in the existence
of positive real solutions of our system for all choices of coefficients
subject to our sign conditions. We give a decision procedure for the existence
of such solutions. In the positive case our procedure yields a parametric
positive solution as a rational function in the coefficients. Our framework
allows to reformulate heuristic subtropical approaches for non-parametric
systems of polynomial inequalities that have been recently used in qualitative
biological network analysis and, independently, in satisfiability modulo theory
solving. We apply our results to characterize the incompleteness of those
methods.

With the goal of lifting model-based guidance from the propositional setting to first-
order logic, I have developed an approximation theorem proving approach based on
counterexample-guided abstraction refinement. A given clause set is transformed
into a simplified form where satisfiability is decidable. This approximation extends
the signature and preserves unsatisfiability: if the simplified clause set is satisfi-
able, so is the original clause set. A resolution refutation generated by a decision
procedure on the simplified clause set can then either be lifted to a refutation in
the original clause set, or it guides a refinement excluding the previously found
unliftable refutation. This way the approach is refutationally complete.
The monadic shallow linear Horn fragment, which is the initial target of the
approximation, is well-known to be decidable. It was a long standing open prob-
lem how to extend the fragment to the non-Horn case, preserving decidability, that
would, e.g., enable to express non-determinism in protocols. I have now proven de-
cidability of the non-Horn monadic shallow linear fragment via ordered resolution.
I further extend the clause language with a new type of constraints, called
straight dismatching constraints. The extended clause language is motivated by an
improved refinement of the approximation-refinement framework. All needed oper-
ations on straight dismatching constraints take linear or linear logarithmic time in
the size of the constraint. Ordered resolution with straight dismatching constraints
is sound and complete and the monadic shallow linear fragment with straight dis-
matching constraints is decidable.
I have implemented my approach based on the SPASS theorem prover. On cer-
tain satisfiable problems, the implementation shows the ability to beat established
provers such as SPASS, iProver, and Vampire.

Satisfiability modulo theories (SMT) solvers have throughout the years been
able to cope with increasingly expressive formulas, from ground logics to full
first-order logic modulo theories. Nevertheless, higher-order logic within SMT
is still little explored. One main goal of the Matryoshka project, which
started in March 2017, is to extend the reasoning capabilities of SMT solvers
and other automatic provers beyond first-order logic. In this preliminary
report, we report on an extension of the SMT-LIB language, the standard input
format of SMT solvers, to handle higher-order constructs. We also discuss how
to augment the proof format of the SMT solver veriT to accommodate these new
constructs and the solving techniques they require.

We consider the problem of determining multiple steady states for positive

real values in models of biological networks. Investigating the potential for

these in models of the mitogen-activated protein kinases (MAPK) network has

consumed considerable effort using special insights into the structure of

corresponding models. Here we apply combinations of symbolic computation

methods for mixed equality/inequality systems, specifically virtual

substitution, lazy real triangularization and cylindrical algebraic

decomposition. We determine multistationarity of an 11-dimensional MAPK network

when numeric values are known for all but potentially one parameter. More

precisely, our considered model has 11 equations in 11 variables and 19

parameters, 3 of which are of interest for symbolic treatment, and furthermore

positivity conditions on all variables and parameters.

We investigate models of the mitogenactivated protein kinases (MAPK) network,

with the aim of determining where in parameter space there exist multiple

positive steady states. We build on recent progress which combines various

symbolic computation methods for mixed systems of equalities and inequalities.

We demonstrate that those techniques benefit tremendously from a newly

implemented graph theoretical symbolic preprocessing method. We compare

computation times and quality of results of numerical continuation methods with

our symbolic approach before and after the application of our preprocessing.

Quantifier-free nonlinear arithmetic (QF_NRA) appears in many applications of

satisfiability modulo theories solving (SMT). Accordingly, efficient reasoning

for corresponding constraints in SMT theory solvers is highly relevant. We

propose a new incomplete but efficient and terminating method to identify

satisfiable instances. The method is derived from the subtropical method

recently introduced in the context of symbolic computation for computing real

zeros of single very large multivariate polynomials. Our method takes as input

conjunctions of strict polynomial inequalities, which represent more than 40%

of the QF_NRA section of the SMT-LIB library of benchmarks. The method takes an

abstraction of polynomials as exponent vectors over the natural numbers tagged

with the signs of the corresponding coefficients. It then uses, in turn, SMT to

solve linear problems over the reals to heuristically find suitable points that

translate back to satisfying points for the original problem. Systematic

experiments on the SMT-LIB demonstrate that our method is not a sufficiently

strong decision procedure by itself but a valuable heuristic to use within a

portfolio of techniques.

In general, first-order predicate logic extended with linear integer

arithmetic is undecidable. We show that the Bernays-Sch\"onfinkel-Ramsey

fragment ($\exists^* \forall^*$-sentences) extended with a restricted form of

linear integer arithmetic is decidable via finite ground instantiation. The

identified ground instances can be employed to restrict the search space of

existing automated reasoning procedures considerably, e.g., when reasoning

about quantified properties of array data structures formalized in Bradley,

Manna, and Sipma's array property fragment. Typically, decision procedures for

the array property fragment are based on an exhaustive instantiation of

universally quantified array indices with all the ground index terms that occur

in the formula at hand. Our results reveal that one can get along with

significantly fewer instances.

The first-order theory of addition over the natural numbers, known as

Presburger arithmetic, is decidable in double exponential time. Adding an

uninterpreted unary predicate to the language leads to an undecidable theory.

We sharpen the known boundary between decidable and undecidable in that we show

that the purely universal fragment of the extended theory is already

undecidable. Our proof is based on a reduction of the halting problem for

two-counter machines to unsatisfiability of sentences in the extended language

of Presburger arithmetic that does not use existential quantification. On the

other hand, we argue that a single $\forall\exists$ quantifier alternation

turns the set of satisfiable sentences of the extended language into a

$\Sigma^1_1$-complete set. Some of the mentioned results can be transfered to

the realm of linear arithmetic over the ordered real numbers. This concerns the

undecidability of the purely universal fragment and the $\Sigma^1_1$-hardness

for sentences with at least one quantifier alternation. Finally, we discuss the

relevance of our results to verification. In particular, we derive

undecidability results for quantified fragments of separation logic, the theory

of arrays, and combinations of the theory of equality over uninterpreted

functions with restricted forms of integer arithmetic. In certain cases our

results even imply the absence of sound and complete deductive calculi.

Rule-based configuration systems are being successfully used in industry, such as DOPLER at Siemens. Those systems make complex domain knowledge available to users and let them derive valid, customized products out of large sets of components. However, maintenance of such systems remains a challenge. Formal models are a prerequisite for the use of automated methods of analysis. This thesis deals with the formalization of rule-based configuration. We develop two logics whose transition semantics are suited for expressing the way systems like DOPLER operate. This is due to the existence of two types of transitions, namely user and rule transitions, and a fixpoint mechanism that determines their dynamic relationship. The first logic, PIDL, models propositional systems, while the second logic, PIDL+, additionally considers arithmetic constraints. They allow the formulation and automated verification of relevant properties of rule- based configuration systems.

The monadic shallow linear Horn fragment is well-known to be decidable and

has many application, e.g., in security protocol analysis, tree automata, or

abstraction refinement. It was a long standing open problem how to extend the

fragment to the non-Horn case, preserving decidability, that would, e.g.,

enable to express non-determinism in protocols. We prove decidability of the

non-Horn monadic shallow linear fragment via ordered resolution further

extended with dismatching constraints and discuss some applications of the new

decidable fragment.

First-order linear real arithmetic enriched with uninterpreted predicate
symbols yields an interesting modeling language. However, satisfiability of
such formulas is undecidable, even if we restrict the uninterpreted predicate
symbols to arity one. In order to find decidable fragments of this language, it
is necessary to restrict the expressiveness of the arithmetic part. One
possible path is to confine arithmetic expressions to difference constraints of
the form $x - y \mathrel{\#} c$, where $\#$ ranges over the standard relations
$<, \leq, =, \neq, \geq, >$ and $x,y$ are universally quantified. However, it
is known that combining difference constraints with uninterpreted predicate
symbols yields an undecidable satisfiability problem again. In this paper, it
is shown that satisfiability becomes decidable if we in addition bound the
ranges of universally quantified variables. As bounded intervals over the reals
still comprise infinitely many values, a trivial instantiation procedure is not
sufficient to solve the problem.

Recently, the separated fragment (SF) of first-order logic has been
introduced. Its defining principle is that universally and existentially
quantified variables may not occur together in atoms. SF properly generalizes
both the Bernays-Sch\"onfinkel-Ramsey (BSR) fragment and the relational monadic
fragment. In this paper the restrictions on variable occurrences in SF
sentences are relaxed such that universally and existentially quantified
variables may occur together in the same atom under certain conditions. Still,
satisfiability can be decided. This result is established in two ways: firstly,
by an effective equivalence-preserving translation into the BSR fragment, and,
secondly, by a model-theoretic argument.
Slight modifications to the described concepts facilitate the definition of
other decidable classes of first-order sentences. The paper presents a second
fragment which is novel, has a decidable satisfiability problem, and properly
contains the Ackermann fragment and---once more---the relational monadic
fragment. The definition is again characterized by restrictions on the
occurrences of variables in atoms. More precisely, after certain
transformations, Skolemization yields only unary functions and constants, and
every atom contains at most one universally quantified variable. An effective
satisfiability-preserving translation into the monadic fragment is devised and
employed to prove decidability of the associated satisfiability problem.

Recently, the separated fragment (SF) has been introduced and proved to be

decidable. Its defining principle is that universally and existentially

quantified variables may not occur together in atoms. The known upper bound on

the time required to decide SF's satisfiability problem is formulated in terms

of quantifier alternations: Given an SF sentence $\exists \vec{z} \forall

\vec{x}_1 \exists \vec{y}_1 \ldots \forall \vec{x}_n \exists \vec{y}_n . \psi$

in which $\psi$ is quantifier free, satisfiability can be decided in

nondeterministic $n$-fold exponential time. In the present paper, we conduct a

more fine-grained analysis of the complexity of SF-satisfiability. We derive an

upper and a lower bound in terms of the degree of interaction of existential

variables (short: degree)}---a novel measure of how many separate existential

quantifier blocks in a sentence are connected via joint occurrences of

variables in atoms. Our main result is the $k$-NEXPTIME-completeness of the

satisfiability problem for the set $SF_{\leq k}$ of all SF sentences that have

degree $k$ or smaller. Consequently, we show that SF-satisfiability is

non-elementary in general, since SF is defined without restrictions on the

degree. Beyond trivial lower bounds, nothing has been known about the hardness

of SF-satisfiability so far.

Proof assistants are becoming widespread for formalization of theories both in computer science and mathematics. They provide rich logics with powerful type systems and machine-checked proofs which increase the confidence in the correctness in complicated and detailed proofs.
However, they incur a significant overhead compared to pen-and-paper proofs.
This thesis describes work on bridging the gap between high-order proof assistants and first-order automated theorem provers by extending the capabilities of the automated theorem provers to provide features usually found in proof assistants.
My first contribution is the development and implementation of a first-order superposition calculus with a polymorphic type system that supports type classes and the accompanying refutational completeness proof for that calculus. The inclusion of the type system into the superposition calculus and solvers completely removes the type encoding overhead when encoding problems from many proof assistants.
My second contribution is the development of SupInd, an extension of the typed superposition calculus that supports data types and structural induction over those data types. It includes heuristics that guide the induction and conjecture strengthening techniques, which can be applied independently of the underlying calculus.
I have implemented the contributions in a tool called Pirate. The evaluations of both contributions show promising results.

Symbolic Computation and Satisfiability Checking are two research areas, both

having their individual scientific focus but sharing also common interests in

the development, implementation and application of decision procedures for

arithmetic theories. Despite their commonalities, the two communities are

rather weakly connected. The aim of our newly accepted SC-square project

(H2020-FETOPEN-CSA) is to strengthen the connection between these communities

by creating common platforms, initiating interaction and exchange, identifying

common challenges, and developing a common roadmap from theory along the way to

tools and (industrial) applications. In this paper we report on the aims and on

the first activities of this project, and formalise some relevant challenges

for the unified SC-square community.

Symbolic Computation and Satisfiability Checking are viewed as individual

research areas, but they share common interests in the development,

implementation and application of decision procedures for arithmetic theories.

Despite these commonalities, the two communities are currently only weakly

connected. We introduce a new project SC-square to build a joint community in

this area, supported by a newly accepted EU (H2020-FETOPEN-CSA) project of the

same name. We aim to strengthen the connection between these communities by

creating common platforms, initiating interaction and exchange, identifying

common challenges, and developing a common roadmap. This abstract and

accompanying poster describes the motivation and aims for the project, and

reports on the first activities.

This paper provides a suite of optimization techniques for

the verification of safety properties of linear hybrid

automata with large discrete state spaces, such as

naturally arising when incorporating health state

monitoring and degradation levels into the controller

design. Such models can -- in contrast to purely functional

controller models -- not analyzed with hybrid verification

engines relying on explicit representations of modes, but

require fully symbolic representations for both the

continuous and discrete part of the state space. The

optimization techniques shown yield consistently a speedup

of about 20 against previously published results for a

similar benchmark suite, and complement these with new

results on counterexample guided abstraction refinement. In

combination with the methods guaranteeing preciseness of

abstractions, this allows to significantly extend the class

of models for which safety can be established, covering in

particular models with 23 continuous variables and 2 to the

71 discrete states, 20 continuous variables and 2 to the

199 discrete states, and 9 continuous variables and 2 to

the 271 discrete states.

A distributed hash table (DHT) is a peer-to-peer network that offers the function of a classic hash table, but where different key-value pairs are stored at different nodes on the network. Like a classic hash table, the main function provided by a DHT is key lookup, which retrieves the value stored at a given key.
Examples of DHT protocols include Chord, Pastry, Kademlia and Tapestry.
Such DHT protocols certain correctness and performance guarantees, but formal verification typically discovers border cases that violate those guarantees. In his PhD thesis, Tianxiang Lu reported correctness problems in published versions of Pastry and developed a model called LuPastry, for which he provided a partial proof of correct delivery of lookup messages assuming no node failure, mechanized in the TLA+ Proof System. In analyzing Lu's proof, I discovered that it contained unproven assumptions, and found counterexamples to several of these assumptions. The contribution of this thesis is threefold. First, I present LuPastry+, a revised TLA+ specification of LuPastry. Aside from needed bug fixes, LuPastry+ contains new definitions that make the specification more modular and significantly improve proof automation. Second, I present a complete TLA+ proof of correct delivery for LuPastry+. Third, I prove that the final step of the node join process of LuPastry/LuPastry+ is not necessary to achieve consistency. In particular, I develop a new specification with a simpler node join process, which I denote by Simplified LuPastry+, and prove correct delivery of lookup messages for this new specification. The proof of correctness of Simplified LuPastry+ is written by reusing the proof for LuPastry+, which represents a success story in proof reuse, especially for proofs of this size.
Each of the two proofs amounts to over 32,000 proof steps; to my knowledge, they are currently the largest proofs written in the TLA+ language, and---together with Lu's proof---the only examples of applying full theorem proving for the verification of DHT protocols

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.

Nunchaku is a new higher-order counterexample generator based on a sequence

of transformations from polymorphic higher-order logic to first-order logic.

Unlike its predecessor Nitpick for Isabelle, it is designed as a stand-alone

tool, with frontends for various proof assistants. In this short paper, we

present some ideas to extend Nunchaku with partial support for dependent types

and type classes, to make frontends for Coq and other systems based on

dependent type theory more useful.

We consider existential problems over the reals. Extended quantifier

elimination generalizes the concept of regular quantifier elimination by

providing in addition answers, which are descriptions of possible assignments

for the quantified variables. Implementations of extended quantifier

elimination via virtual substitution have been successfully applied to various

problems in science and engineering. So far, the answers produced by these

implementations included infinitesimal and infinite numbers, which are hard to

interpret in practice. We introduce here a post-processing procedure to

convert, for fixed parameters, all answers into standard real numbers. The

relevance of our procedure is demonstrated by application of our implementation

to various examples from the literature, where it significantly improves the

quality of the results.

We introduce a new decidable fragment of first-order logic with equality,

which strictly generalizes two already well-known ones -- the

Bernays-Sch\"onfinkel-Ramsey (BSR) Fragment and the Monadic Fragment. The

defining principle is the syntactic separation of universally quantified

variables from existentially quantified ones at the level of atoms. Thus, our

classification neither rests on restrictions on quantifier prefixes (as in the

BSR case) nor on restrictions on the arity of predicate symbols (as in the

monadic case). We demonstrate that the new fragment exhibits the finite model

property and derive a non-elementary upper bound on the computing time required

for deciding satisfiability in the new fragment. For the subfragment of prenex

sentences with the quantifier prefix $\exists^* \forall^* \exists^*$ the

satisfiability problem is shown to be complete for NEXPTIME. Finally, we

discuss how automated reasoning procedures can take advantage of our results.

We combine key ideas from first-order superposition and propositional CDCL to

create the new calculus NRCL deciding the Bernays-Sch\"onfinkel fragment. It

inherits the abstract redundancy criterion and the monotone model operator from

superposition. CDCL adds to NRCL the dynamic, conflict-driven search for an

atom ordering inducing a model. As a result, in NRCL a false clause can be

effectively found modulo the current model assumption. It guides the derivation

of a first-order ordered resolvent that is never redundant. Similar to

1UIP-learning in CDCL, the learned resolvent induces backtracking and via

propagation blocks the previous conflict state for the rest of the search.

Since learned clauses are never redundant, only finitely many can be generated

by NRCL on the Bernays-Sch\"onfinkel fragment, which provides a nice argument

for termination.

In this paper, we present an algorithm for computing a fundamental matrix of

formal solutions of completely integrable Pfaffian systems with normal

crossings in several variables. This algorithm is a generalization of a method

developed for the bivariate case based on a combination of several reduction

techniques and is implemented in the computer algebra system Maple.

This paper presents a formalized framework for defining corecursive functions

safely in a total setting, based on corecursion up-to and relational

parametricity. The end product is a general corecursor that allows corecursive

(and even recursive) calls under well-behaved operations, including

constructors. Corecursive functions that are well behaved can be registered as

such, thereby increasing the corecursor's expressiveness. The metatheory is

formalized in the Isabelle proof assistant and forms the core of a prototype

tool. The corecursor is derived from first principles, without requiring new

axioms or extensions of the logic.

We consider feasibility of linear integer programs in the context of

verification systems such as SMT solvers or theorem provers. Although

satisfiability of linear integer programs is decidable, many state-of-the-art

solvers neglect termination in favor of efficiency. It is challenging to design

a solver that is both terminating and practically efficient. Recent work by

Jovanovic and de Moura constitutes an important step into this direction. Their

algorithm CUTSAT is sound, but does not terminate, in general. In this paper we

extend their CUTSAT algorithm by refined inference rules, a new type of

conflicting core, and a dedicated rule application strategy. This leads to our

algorithm CUTSAT++, which guarantees termination.

Some recent methods for lossy signal and image compression store only a few

selected pixels and fill in the missing structures by inpainting with a partial

differential equation (PDE). Suitable operators include the Laplacian, the

biharmonic operator, and edge-enhancing anisotropic diffusion (EED). The

quality of such approaches depends substantially on the selection of the data

that is kept. Optimising this data in the domain and codomain gives rise to

challenging mathematical problems that shall be addressed in our work.

In the 1D case, we prove results that provide insights into the difficulty of

this problem, and we give evidence that a splitting into spatial and tonal

(i.e. function value) optimisation does hardly deteriorate the results. In the

2D setting, we present generic algorithms that achieve a high reconstruction

quality even if the specified data is very sparse. To optimise the spatial

data, we use a probabilistic sparsification, followed by a nonlocal pixel

exchange that avoids getting trapped in bad local optima. After this spatial

optimisation we perform a tonal optimisation that modifies the function values

in order to reduce the global reconstruction error. For homogeneous diffusion

inpainting, this comes down to a least squares problem for which we prove that

it has a unique solution. We demonstrate that it can be found efficiently with

a gradient descent approach that is accelerated with fast explicit diffusion

(FED) cycles. Our framework allows to specify the desired density of the

inpainting mask a priori. Moreover, is more generic than other data

optimisation approaches for the sparse inpainting problem, since it can also be

extended to nonlinear inpainting operators such as EED. This is exploited to

achieve reconstructions with state-of-the-art quality.

We also give an extensive literature survey on PDE-based image compression

methods.