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

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Effective Quantifier Elimination and Decision - Theory, Implementations, Applications, Perspectives
Speaker:Thomas Sturm
coming from:Max-Planck-Institut für Informatik - RG 1
Speakers Bio:
Event Type:Antrittsvorlesung
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:Public Audience
Date, Time and Location
Date:Wednesday, 24 July 2013
Duration:45 Minutes
Building:E1 7
Effective quantifier elimination procedures for first-order theories provide a

powerful tool for generically solving a wide range of problems based on logical
specifications. In contrast to general first-order provers, quantifier
elimination procedures are based on a fixed set of admissible logical symbols
with an implicitly fixed semantics. This admits the use of sub-algorithms from
symbolic computation. We are going to focus on real quantifier elimination and
its applications giving examples from geometry and verification. Beyond
quantifier elimination we are going to sketch work-in-progress on an incomplete
decision procedure for the existential fragment of the reals, which has been
successfully applied to the analysis of chemical reaction systems. We conclude
with an overview on quantifier-eliminable theories that have been realized in
our open-source computer logic software Redlog (

Name(s):Jennifer Müller
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Attachments, File(s):
  • Jennifer Müller, 07/16/2013 11:31 AM -- Created document.