Max-Planck-Institut für Informatik
max planck institut
informatik
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
Language:English
Date, Time and Location
Date:Wednesday, 24 July 2013
Time:14:15
Duration:45 Minutes
Location:Saarbrücken
Building:E1 7
Room:0.01
Abstract
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 (www.redlog.eu).

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