Campus Event Calendar
Event Entry
What and Who
Superposition and Decision Procedures Back and Forth
Thomas Hillenbrand
Max-Planck-Institut für Informatik - RG 1
Promotionskolloquium
AG 1, AG 3, AG 4, AG 5, SWS, RG1, MMCI
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 24 April 2009
16:00
-- Not specified --
E1 4
024
Saarbrücken
Abstract
Two apparently different approaches to automating deduction are mentioned in the title of the thesis; 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: Superposition can be, firstly, run on top of decision
procedures; secondly, employed as proof-theoretic means underneath combined decision procedures; and thirdly, used as a decision procedure
for many interesting theories, turning a big engine into a little one.
"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: Superposition can be, firstly, run on top of decision
procedures; secondly, employed as proof-theoretic means underneath combined decision procedures; and thirdly, used as a decision procedure
for many interesting theories, turning a big engine into a little one.
Contact
Jennifer Müller
900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 04/21/2009 11:25 -- Created document.