Datensatz

Zusammenfassung

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.