Zimmer, Stephan

Intelligent Combination of a First Order Theorem Prover and {SMT} Procedures

First-order logic combined with arithmetic background theories is a
powerful tool for representing and managing huge amounts of
declarative information. Special fragments of it were successfully
applied to manifold problems from different areas of computer
science. From an automated reasoning perspective, however, this
expressiveness makes it particular challenging to develop theorem
provers that can deal with general classes of those languages:
General purpose theorem provers on the one hand cannot cope
efficiently with arithmetic and specialized decision procedures on
the other hand are notoriously bad at dealing with quantifiers, if
they are even supported at all.

The SPASS+T system, which was developed by Prevosto and Waldmann,
aims to attack this problem by combining the superposition-based
theorem prover SPASS with decision procedures for linear arithmetic
and free function symbols; furthermore, the set of standard
first-order inference and reduction rules is complemented by
specialized rules for arithmetic.

In this work we present various extensions to their initial
implementation. The main task of the thesis was to stretch the
capabilities of the system by integrating the SPASS splitting rule,
which had to be switched off so far. Splitting is highly efficient
for SPASS and has also advantages in a combination like SPASS+T. In
order to add support for splitting in SPASS+T we first revised the
previous system architecture and developed an advanced coupling
between SPASS and the SMT procedure and achieved a tighter
integration of the latter in form of a new inference rule.
Furthermore, for splitting a careful analysis of the different
prover configurations was necessary. Besides splitting, the new
coupling also allows to use the SPASS proof documentation mode
regarding subproofs that were contributed by the SMT procedure. The
documented proofs can be automatically certified. To this end we
extended the existing SPASS proof validator in such a way that it
also employs an external SMT procedure and now can verify, besides
ordinary first-order proof steps, arithmetic inferences as well. In
order to improve the built-in arithmetic simplification rules of
SPASS+T and let them also work with bignums and rational numbers, we
integrated the GNU multiple precision library. Finally, we added a
new reduction rule that deals with clauses which impose lower or
upper bounds on a variable.

We will describe all these extensions in detail, discuss their
impact on the system architecture, and demonstrate the capabilities
of the system by applying it to some examples.