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.

We generalize several propositional preprocessing techniques to higher-order
logic, building on existing first-order generalizations. These techniques
eliminate literals, clauses, or predicate symbols from the problem, with the
aim of making it more amenable to automatic proof search. We also introduce a
new technique, which we call quasipure literal elimination, that strictly
subsumes pure literal elimination. The new techniques are implemented in the
Zipperposition theorem prover. Our evaluation shows that they sometimes help
prove problems originating from the TPTP library and Isabelle formalizations.

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.

We generalize the framework of virtual substitution for real quantifier

elimination to arbitrary but bounded degrees. We make explicit the

representation of test points in elimination sets using roots of parametric

univariate polynomials described by Thom codes. Our approach follows an early

suggestion by Weispfenning, which has never been carried out explicitly.

Inspired by virtual substitution for linear formulas, we show how to

systematically construct elimination sets containing only test points

representing lower bounds.

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 describe a new incomplete but terminating method for real root finding for

large multivariate polynomials. We take an abstract view of the polynomial as

the set of exponent vectors associated with sign information on the

coefficients. Then we employ linear programming to heuristically find roots.

There is a specialized variant for roots with exclusively positive coordinates,

which is of considerable interest for applications in chemistry and systems

biology. An implementation of our method combining the computer algebra system

Reduce with the linear programming solver Gurobi has been successfully applied

to input data originating from established mathematical models used in these

areas. We have solved several hundred problems with up to more than 800000

monomials in up to 10 variables with degrees up to 12. Our method has failed

due to its incompleteness in less than 8 percent of the cases.

Counterexample-guided abstraction refinement is a well-established technique

in verification. In this paper we instantiate the idea for first-order logic

theorem proving. Given a clause set $N$ we propose its abstraction into a

clause set $N'$ belonging to a decidable first-order fragment. The abstraction

preserves satisfiability: if $N'$ is satisfiable, so is $N$. A refutation in

$N'$ can then either be lifted to a refutation in $N$, or it guides a

refinement of $N$ and its abstraction $N'$ excluding the previously found

refutation that is not liftable.

Linear arithmetic extended with free predicate symbols is undecidable, in

general. We show that the restriction of linear arithmetic inequations to

simple bounds extended with the Bernays-Sch\"onfinkel-Ramsey free first-order

fragment is decidable and NEXPTIME-complete. The result is almost tight because

the Bernays-Sch\"onfinkel-Ramsey fragment is undecidable in combination with

linear difference inequations, simple additive inequations, quotient

inequations and multiplicative inequations.

This report documents the program and the outcomes of Dagstuhl Seminar 13411 "Deduction and Arithmetic". The aim of this seminar was to bring together researchers working in deduction and fields related to arithmetic constraint solving. Current research in deduction can be categorized in three main strands: SMT solvers, automated first-order provers, and interactive provers. Although dealing with arithmetic has been in focus of all three for some years, there is still need of much better support of arithmetic. Reasong about arithmetic will stay at the center of attention in all three main approaches to automated deduction during the coming five to ten years. The seminar was an important event for the subcommunities involved that made it possible to communicate with each other so as to avoid duplicate effort and to exploit synergies. It succeeded also in identifying a number of important trends and open problems.

In this paper we study theory combinations over non-disjoint

signatures in which hierarchical and modular reasoning is

possible. We use a notion of locality of a theory extension

parameterized by a closure operator on ground terms.

We give criteria for recognizing these types of theory

extensions. We then show that combinations of extensions of

theories which are local in this extended sense have also a

locality property and hence allow modular and hierarchical

reasoning. We thus obtain parameterized decidability and

complexity results for many (combinations of) theories

important in verification.

We consider satisfiability modulo theory-solving for linear real arithmetic. Inspired by related work for the Fourier–Motzkin method, we combine virtual substitution with learning strategies. For the first time, we present virtual substitution—including our learning strategies—as a formal calculus. We prove soundness and completeness for that calculus. Some standard linear programming benchmarks computed with an experimental implementation of our calculus show that the integration of learning techniques into virtual substitution gives rise to considerable speedups. Our implementation is open-source and freely available.

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 a new completeness result for the fragment where

all background-sorted terms are ground.

In this paper we study possibilities of using methods for

hierarchical reasoning in local theory extensions for the

analysis and verification of parametric hybrid systems,

where the parameters can be either constants or functions.

Our goal is to automatically provide guarantees that such

systems satisfy certain safety or invariance conditions.

We first analyze the possibility of automatically generating

such guarantees in the form of constraints on parameters,

then show that we can also synthesise so-called criticality

functions, typically used for proving stability and/or

safety of hybrid systems.

We illustrate our methods on several examples.

Rule-based specifications of systems have again

become common in the context of product line variability modeling and

configuration systems. In this paper, we define a logical

foundation for rule-based specifications that has enough expressivity

and operational behavior to be

practically useful and at the same time enables decidability of

important overall properties such as consistency or cycle-freeness.

Our logic supports rule-based interactive user transitions as well as

the definition of a domain theory via rule transitions.

As a running example, we model DOPLER, a rule-based configuration system

currently in use at Siemens.

The success of superposition-based theorem proving in first-order logic relies

in particular on the fact that the superposition calculus can be turned into a

decision procedure for various decidable fragments of first-order logic and has

been successfully used to identify new decidable classes. In this paper, we

extend this story to the hierarchic combination of linear arithmetic and

first-order superposition. We show that decidability of reachability in timed

automata can be obtained by instantiation of an abstract termination result for

SUP(LA), the hierarchic combination of linear arithmetic and first-order

superposition.

In this paper we present a method for obtaining local sets of clauses from

possibly non-local ones. For this, we follow the work of Basin and Ganzinger

and use saturation under a version of ordered resolution. In order to address

the fact that saturation can generate infinite sets of clauses, we use

constrained clauses and show that a link can be established

between saturation and locality also for constrained clauses:

This often allows us to give a finite representation

of possibly infinite saturated sets of clauses.

Data-parallel languages like OpenCL and CUDA are an important means to exploit

the computational power of today's computing devices.

We consider the compilation of such languages for CPUs with SIMD instruction

sets.

To generate efficient code, one wants to statically decide whether or not

certain

memory operations access consecutive addresses.

We formalize the notion of consecutivity and algorithmically reduce the static

decision to satisfiability problems in Presburger Arithmetic.

We introduce a preprocessing technique on these SMT problems, which makes it

feasible to apply an off-the-shelf SMT solver.

We show that a prototypical OpenCL CPU driver based on our approach generates

more efficient code than any other state-of-the-art driver.

BDI (Bounded Depth Increase) is a new decidable first-order clause class. It strictly includes known classes such as PVD. The arity of function and predicate symbols as well as the shape of atoms is not restricted in BDI. Instead the shape of "cycles" in resolution inferences is restricted such that the depth of generated clauses may increase but is still finitely bound. The BDI class is motivated by real world problems where function terms are used to represent record structures.

We show that the hyper-resolution calculus modulo redundancy elimination terminates on BDI clause sets. Employing this result to the ordered resolution calculus, we can also prove termination of ordered resolution on BDI, yielding a more efficient decision procedure.

In this paper we study possibilities of using methods for

hierarchical reasoning in local theory extensions for the

analysis and verification of parametric hybrid systems,

where the parameters can be either constants or functions.

Our goal is to automatically provide guarantees that such

systems satisfy certain safety or invariance conditions.

We first analyze the possibility of automatically generating

such guarantees in the form of constraints on parameters,

then show that we can also synthesise so-called criticality

functions, typically used for proving stability and/or

safety of hybrid systems.

We illustrate our methods on several examples.

Many problems in mathematics and computer science can be

reduced to proving the satisfiability of conjunctions of

literals in a background theory which is often the extension

of a base theory with additional functions or a combination

of theories.

It is therefore important to have efficient procedures for

checking satisfiability of conjunctions of ground literals

in extensions and combinations of theories.

For a special type of theory extensions, namely \em local

extensions, hierarchic reasoning, in which a theorem prover

for the base theory can be used as a ``black box'',

is possible. Many theories used in computer science or

mathematics are local extensions of a base theory.

However, often it is necessary to consider complex extensions

of a theory, with various types of functions.

In this paper we identify situations in which

a combination of local extensions of a base theory

is guaranteed to be again a local extension of the base theory.

We thus obtain criteria both for recognizing wider classes of

local theory extensions, and for modular reasoning in

combinations of theories over non-disjoint signatures.

In this paper we show that subsumption problems in the description logics EL and EL+ can be expressed as uniform word problems in classes of semilattices with monotone operators. We use possibilities of efficient local reasoning in such classes of algebras, to obtain uniform PTIME decision procedures for TBox and CBox subsumption in EL and EL+. These locality considerations allow us to present a new family of (possibly many-sorted) logics which extend EL and EL+ with n-ary roles and/or numerical domains.

We propose an improvement of the famous IC3 algorithm for model checking

safety properties of finite state systems. We collect models computed by the

SAT-solver during the clause propagation phase of the algorithm and use them as

witnesses for why the respective clauses could not be pushed forward. It only

makes sense to recheck a particular clause for pushing when its witnessing

model falsifies a newly added clause. Since this trigger test is both

computationally cheap and sufficiently precise, we can afford to keep clauses

pushed as far as possible at all times. Experiments indicate that this strategy

considerably improves IC3's performance.

The hierarchic combination of linear arithmetic and firstorder

logic with free function symbols, FOL(LA), results in a strictly

more expressive logic than its two parts. The SUP(LA) calculus can be

turned into a decision procedure for interesting fragments of FOL(LA).

For example, reachability problems for timed automata can be decided

by SUP(LA) using an appropriate translation into FOL(LA). In this paper,

we extend the SUP(LA) calculus with an additional inference rule,

automatically generating inductive invariants from partial SUP(LA)

derivations. The rule enables decidability of more expressive fragments,

including reachability for timed automata with unbounded integer variables.

We have implemented the rule in the SPASS(LA) theorem prover

with promising results, showing that it can considerably speed up proof

search and enable termination of saturation for practically relevant

problems.

The hierarchic combination of linear arithmetic and firstorder

logic with free function symbols, FOL(LA), results in a strictly

more expressive logic than its two parts. The SUP(LA) calculus can be

turned into a decision procedure for interesting fragments of FOL(LA).

For example, reachability problems for timed automata can be decided

by SUP(LA) using an appropriate translation into FOL(LA). In this paper,

we extend the SUP(LA) calculus with an additional inference rule,

automatically generating inductive invariants from partial SUP(LA)

derivations. The rule enables decidability of more expressive fragments,

including reachability for timed automata with unbounded integer variables.

We have implemented the rule in the SPASS(LA) theorem prover

with promising results, showing that it can considerably speed up proof

search and enable termination of saturation for practically relevant

problems.

The hierarchic superposition calculus over a theory T, called SUP(T), enables

sound reasoning on the hierarchic combination

of a theory T with full first-order logic, FOL(T). If a FOL(T) clause set

enjoys a sufficient completeness criterion,

the calculus is even complete. Clause sets over the ground fragment of FOL(T)

are not sufficiently complete, in general.

In this paper we show that any clause set over the ground FOL(T) fragment can

be transformed into a sufficiently complete one,

and prove that SUP(T) terminates on the transformed clause set, hence

constitutes a decision procedure provided the

existential fragment of the theory T is decidable. Thanks to the hierarchic

design of SUP(T), the decidability result

can be extended beyond the ground case. We show SUP(T) is a decision procedure

for the non-ground FOL fragment

plus a theory T, if every non-constant function symbol from the underlying FOL

signature ranges into the sort of the theory T,

and every term of the theory sort is ground. Examples for T are in particular

decidable fragments of arithmetic.

Labelled superposition (LPSup) is a new calculus for PLTL. One of its

distinguishing features, in comparison to other resolution-based approaches, is

its ability to construct partial models on the fly. We use this feature to

design a new decision procedure for the logic, where the models are effectively

used to guide the search. On a representative set of benchmarks, our

implementation is then shown to considerably advance the state of the art.

This paper introduces a new decision procedure for PLTL based on labelled

superposition.

Its main idea is to treat temporal formulas as infinite sets of purely

propositional clauses over an extended signature. These infinite sets are then

represented by finite sets of labelled propositional clauses. The new

representation enables the replacement of the complex temporal resolution

rule, suggested by existing resolution calculi for PLTL, by a fine grained

repetition check of finitely saturated labelled clause sets followed by a

simple inference. The completeness argument is based on the standard model

building idea from superposition. It inherently justifies ordering

restrictions, redundancy elimination and effective partial model building. The

latter can be directly used to effectively generate counterexamples of

non-valid PLTL conjectures out of saturated labelled clause sets in a

straightforward way.

This paper introduces a new decision procedure for PLTL based on labelled

superposition.

Its main idea is to treat temporal formulas as infinite sets of purely

propositional clauses over an extended signature. These infinite sets are then

represented by finite sets of labelled propositional clauses. The new

representation enables the replacement of the complex temporal resolution

rule, suggested by existing resolution calculi for PLTL, by a fine grained

repetition check of finitely saturated labelled clause sets followed by a

simple inference. The completeness argument is based on the standard model

building idea from superposition. It inherently justifies ordering

restrictions, redundancy elimination and effective partial model building. The

latter can be directly used to effectively generate counterexamples of

non-valid PLTL conjectures out of saturated labelled clause sets in a

straightforward way.

We present a new calculus for first-order theorem proving with equality,

ME+Sup, which generalizes both the Superposition calculus and the Model

Evolution calculus (with equality) by integrating their inference rules and

redundancy criteria in a non-trivial way. The main motivation is to combine the

advantageous features of these two rather complementary calculi in a single

framework. In particular, Model Evolution, as a lifted version of the

propositional DPLL procedure, contributes a non-ground splitting rule that

effectively permits to split a clause into \emph{non} variable disjoint

subclauses. In the paper we present the calculus in detail. Our main result is

its completeness under semantically justified redundancy criteria and

simplification rules. We also show how under certain assumptions the model

representation computed by a (finite and fair) derivation can be queried in an

effective way.

In deduction modulo, a theory is not represented by a set of axioms but by a

congruence on propositions modulo which the inference rules of standard

deductive systems---such as for instance natural deduction---are applied.

Therefore, the reasoning that is intrinsic of the theory does not appear in the

length of proofs. In general, the congruence is defined through a rewrite

system over terms and propositions. We define a rigorous framework to study

proof lengths in deduction modulo, where the congruence must be computed in

polynomial time. We show that even very simple rewrite systems lead to

arbitrary proof-length speed-ups in deduction modulo, compared to using axioms.

As higher-order logic can be encoded as a first-order theory in deduction

modulo, we also study how to reinterpret, thanks to deduction modulo, the

speed-ups between higher-order and first-order arithmetics that were stated by

G\"odel. We define a first-order rewrite system with a congruence decidable in

polynomial time such that proofs of higher-order arithmetic can be linearly

translated into first-order arithmetic modulo that system. We also present the

whole higher-order arithmetic as a first-order system without resorting to any

axiom, where proofs have the same length as in the axiomatic presentation.

This paper identifies an industrially relevant class of

linear hybrid automata (LHA) called reasonable LHA for

which parametric verification of convex safety properties

with exhaustive entry states can be verified in polynomial

time and time-bounded reachability can be decided

in nondeterministic polynomial time for non-parametric

verification and in exponential time for

parametric verification. Properties with exhaustive entry

states are restricted to runs originating in

a (specified) inner envelope of some mode-invariant.

Deciding whether an LHA is reasonable is

shown to be decidable in polynomial time.

We study linear hybrid automata with dynamics of the form

$\sum a_i x_i \leq a$ and $\sum b_i {\dot x_i} \leq b$.

We show that verification of safety properties for reasonable

classes of such systems can be reduced to invariant checking

and bounded model checking and, ultimately, to checking the

validity of certain formulae (obtained using a polynomial

reduction).

We show that the problem of checking the validity of the formulae

obtained this way is typically in NP, and identify verification

tasks which can be performed in PTIME.

These reductions can also be used for parametric systems, both

for checking safety properties given constraints on parameters,

and for deriving constraints of parameters that guarantee that

safety properties hold.

This paper identifies an industrially relevant class of

linear hybrid automata (LHA) called reasonable LHA for

which parametric verification of convex safety properties

with exhaustive entry states can be verified in polynomial

time and time-bounded reachability can be decided

in nondeterministic polynomial time for non-parametric

verification and in exponential time for

parametric verification. Properties with exhaustive entry

states are restricted to runs originating in

a (specified) inner envelope of some mode-invariant.

Deciding whether an LHA is reasonable is

shown to be decidable in polynomial time.

We describe an approach to integrate incremental ow pipe computation into a

fully symbolic backward model checker for hybrid systems. Our method combines

the advantages of symbolic state set representation, such as the ability to

deal with large numbers of boolean variables, with an effcient way to handle

continuous ows dened by linear differential equations, possibly including

bounded disturbances.

The first-order theory over non-linear arithmetic

including transcendental functions (NLA) is undecidable.

Nevertheless, in this paper we show that a particular combination

with superposition leads to a sound and complete calculus that

is useful in practice. We follow basically the ideas

of the SUP(LA) combination, but have to take care

of undecidability, resulting in ``unknown'' answers by

the NLA reasoning procedure. A pipeline

of NLA constraint simplification techniques related to

the SUP(NLA) framework significantly decreases the number of ``unknown''

answers.

The resulting approach is implemented as SUP(NLA) by a system combination

of SPASS and iSAT. Applied to various scenarios

of traffic collision avoidance protocols, we show by experiments

that SPASS(iSAT) can fully automatically proof and disproof safety

properties of such protocols using the very same formalization.

We study possibilities of combining (fragments) of the lightweight description

logics ${\cal F}{\cal L}_0$ and

${\cal E}{\cal L}$, and identify classes of subsumption

problems in a combination of ${\cal E}{\cal L}$ and

Horn-${\cal F}{\cal L}_0$, which can be

checked in PSPACE resp. PTIME.

Since ${\cal F}{\cal L}_0$ allows universal role restrictions

and ${\cal E}{\cal L}$ allows existential role restrictions,

we thus have a framework where subsumption between

expressions including both types

of role restrictions (but for disjoint sets of roles) can be checked in

polynomial

space or time.

We consider parametric families of semi-algebraic geometric objects, each

implicitly defined by a first-order formula. Given an unambiguous description

of such an object family and an intended alternative description we

automatically construct a first-order formula which is true if and only if our

alternative description uniquely describes geometric objects of the reference

description. We can decide this formula by applying real quantifier

elimination. In the positive case we furthermore derive the defining

first-order formulas corresponding to our new description. In the negative case

we can produce sample points establishing a counterexample for the uniqueness.

We demonstrate our method by automatically proving uniqueness theorems for

characterizations of several geometric primitives and simple complex objects.

Finally, we focus on tori, characterizations of which can be applied in spline

approximation theory with toric segments. Although we cannot yet practically

solve the fundamental open questions in this area within reasonable time and

space, we demonstrate that they can be formulated in our framework. In addition

this points at an interesting and practically relevant challenge problem for

automated deduction in geometry in general.

Pastry is an algorithm that provides a scalable distributed hash table over

an underlying P2P network. Several implementations of Pastry are available

and have been applied in practice, but no attempt has so far been made to

formally describe the algorithm or to verify its properties. Since Pastry combines

rather complex data structures, asynchronous communication, concurrency,

resilience to churn and fault tolerance, it makes an interesting target

for verication. We have modeled Pastry's core routing algorithms and communication

protocol in the specication language TLA+. In order to validate

the model and to search for bugs we employed the TLA+ model checker tlc

to analyze several qualitative properties. We obtained non-trivial insights in

the behavior of Pastry through the model checking analysis. Furthermore,

we started to verify Pastry using the very same model and the interactive

theorem prover tlaps for TLA+. A rst result is the reduction of global

Pastry correctness properties to invariants of the underlying data structures.

We present the application of real quantifier elimination to formal

verification and synthesis of continuous and switched dynamical systems.

Through a series of case studies, we show how first-order formulas over the

reals arise when formally analyzing models of complex control systems. Existing

off-the-shelf quantifier elimination procedures are not successful in

eliminating quantifiers from many of our benchmarks. We therefore automatically

combine three established software components: virtual subtitution based

quantifier elimination in Reduce/Redlog, cylindrical algebraic decomposition

implemented in Qepcad, and the simplifier Slfq implemented on top of Qepcad. We

use this combination to successfully analyze various models of systems

including adaptive cruise control in automobiles, adaptive flight control

system, and the classical inverted pendulum problem studied in control theory.

We investigate algorithmic methods to tackle the following problem: Given a

system of parametric ordinary differential equations built by a biological

model, does there exist ranges of values for the model parameters and variables

which are both meaningful from a biological point of view and where oscillating

trajectories, can be found? We show that in the common case of polynomial

vector fields known criteria excluding the existence of non-constant limit

cycles lead to quantifier elimination problems over the reals. We apply these

criteria to various models that have been previously investigated in the

context of algebraic biology.

Deduction modulo consists in presenting a theory through rewrite