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

MPI-INF RG1 Publications :: Thesis :: Hillenbrand, Thomas


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 - Doctoral dissertation | @PhdThesis | Doktorarbeit


Author
Author(s)*:Hillenbrand, Thomas
BibTeX citekey*:HillenbrandDiss2008
Language:English

Title, School
Title*:Superposition and Decision Procedures -- Back and Forth
School:Universität des Saarlandes
Type of Thesis*:Doctoral dissertation
Month:October
Year:2008


Note, Abstract, Copyright
LaTeX Abstract:Two apparently different approaches to automating deduction are mentioned in the title; they are the subject of a debate on ``big engines vs.\ little engines of proof''. The contributions in this thesis advocate that these two strands of research can interplay in subtle and sometimes unexpected ways, such that mutual pervasion can lead to intriguing results: Firstly, superposition can be run on top of decision procedures. This we demonstrate for the class of Shostak theories, incorporating a little engine into a big one. As another instance of decision procedures within superposition, we show that ground confluent rewrite systems, which decide entailment problems in equational logic, can be harnessed for detecting redundancies in superposition derivations. Secondly, superposition can be employed as proof-theoretic means underneath combined decision procedures: We re-establish the correctness of the Nelson-Oppen procedure as an instance of the completeness of superposition. Thirdly, superposition can be used as a decision procedure for many interesting theories, turning a big engine into a little one. For the theory of bits and of fixed-size bitvectors, we suggest a rephrased axiomatization combined with a transformation of conjectures, based on which superposition decides the universal fragment. Furthermore, with a modification of lifting, we adapt superposition to the theory of bounded domains and give a decision procedure, which captures the Bernays-Sch\"onfinkel class as well.
Keywords:Automated Reasoning, Superposition, Decision Procedures
Download Access Level:Public
Download File(s):View attachments here:

Referees, Status, Dates
1. Referee:Bernd Finkbeiner
2. Referee:Robert Nieuwenhuis
Supervisor:Christoph Weidenbach
Status:Completed
Date Kolloquium:24 April 2009
Chair Kolloquium:Gert Smolka

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

BibTeX Entry:

@PHDTHESIS{HillenbrandDiss2008,
AUTHOR = {Hillenbrand, Thomas},
TITLE = {Superposition and Decision Procedures -- Back and Forth},
SCHOOL = {Universit{\"a}t des Saarlandes},
YEAR = {2008},
TYPE = {Doctoral dissertation}
MONTH = {October},
}


Hide details for Attachment SectionAttachment Section

View attachments here:




Entry last modified by Thomas Hillenbrand, 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
03/27/2009 12:54:29 PM
Revisions
2.
1.
0.

Editor(s)
Thomas Hillenbrand
Thomas Hillenbrand
Thomas Hillenbrand

Edit Dates
05/08/2009 03:07:46 PM
03/27/2009 12:56:32 PM
03/27/2009 12:54:29 PM