Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-INF RG1 Publications :: Thesis :: Zimmer, Stephan


MPI-INF RG1 Publications
Show all entries of:this year (2019)last year (2018)two years ago (2017)Open in Notes
Action:login to update  Library locked

Thesis - Diploma Thesis | | Diplomarbeit


Author
Author(s)*:Zimmer, Stephan
BibTeX citekey*:Zimmer2007
Language:English

Title, School
Title*:Intelligent Combination of a First Order Theorem Prover and {SMT} Procedures
School:Universität des Saarlandes
Type of Thesis*:Diploma Thesis
Month:December
Year:2007


Note, Abstract, Copyright
LaTeX Abstract: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.

Download Access Level:Intranet

Referees, Status, Dates
1. Referee:Christoph Weidenbach
2. Referee:Uwe Waldmann
Supervisor:Christoph Weidenbach
Status:Completed
Date Kolloquium:25 February 2013

Correlation
MPG Unit:Max-Planck-Institut für Informatik
MPG Subunit:Automation of Logic
Audience:popular
Appearance:MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort


BibTeX Entry:
@MASTERSTHESIS{Zimmer2007,
AUTHOR = {Zimmer, Stephan},
TITLE = {Intelligent Combination of a First Order Theorem Prover and {SMT} Procedures},
SCHOOL = {Universit{\"a}t des Saarlandes},
YEAR = {2007},
TYPE = {Diploma thesis}
MONTH = {December},
}



Entry last modified by Uwe Waldmann, 08/06/2014
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
[Library]
Created
04/14/2008 03:12:12 PM
Revisions
5.
4.
3.
2.
1.
Editor(s)
Uwe Waldmann
Roxane Wetzel
Roxane Wetzel
Roxane Wetzel
Roxane Wetzel
Edit Dates
25.02.2013 21:11:53
16.04.2008 15:01:47
14.04.2008 15:53:36
14.04.2008 15:20:45
14.04.2008 15:17:40