Publications - The Year Before Last

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.