English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
  Superposition and Decision Procedures - Back and Forth

Hillenbrand, T. (2008). Superposition and Decision Procedures - Back and Forth. PhD Thesis, Universität des Saarlandes, Saarbrücken. doi:10.22028/D291-25942.

Item is

Basic

show hide
Genre: Thesis
Latex : Superposition and Decision Procedures -- Back and Forth

Files

show Files
hide Files
:
SupDec.pdf (Any fulltext), 953KB
 
File Permalink:
-
Name:
SupDec.pdf
Description:
-
OA-Status:
Visibility:
Private
MIME-Type / Checksum:
application/pdf
Technical Metadata:
Copyright Date:
-
Copyright Info:
-
License:
-

Locators

show
hide
Description:
-
OA-Status:
Green
Locator:
http://scidok.sulb.uni-saarland.de/doku/lic_ohne_pod.php?la=de (Copyright transfer agreement)
Description:
-
OA-Status:
Not specified

Creators

show
hide
 Creators:
Hillenbrand, Thomas1, 2, Author           
Weidenbach, Christoph1, Advisor                 
Finkbeiner, Bernd3, Referee
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              
2International Max Planck Research School, MPI for Informatics, Max Planck Society, Campus E1 4, 66123 Saarbrücken, DE, ou_1116551              
3External Organizations, ou_persistent22              

Content

show
hide
Free keywords: -
 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önfinkel class as well.

Details

show
hide
Language(s): eng - English
 Dates: 2009-04-2420082008
 Publication Status: Issued
 Pages: -
 Publishing info: Saarbrücken : Universität des Saarlandes
 Table of Contents: -
 Rev. Type: -
 Identifiers: BibTex Citekey: HillenbrandDiss2008
DOI: 10.22028/D291-25942
URN: urn:nbn:de:bsz:291-scidok-24190
Other: hdl:20.500.11880/25998
 Degree: PhD

Event

show

Legal Case

show

Project information

show

Source

show