MPI-INF Logo
Campus Event Calendar

Event Entry

What and Who

Effective Quantifier Elimination and Decision - Theory, Implementations, Applications, Perspectives

Thomas Sturm
Max-Planck-Institut für Informatik - RG 1
Antrittsvorlesung
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI  
Public Audience
English

Date, Time and Location

Wednesday, 24 July 2013
14:15
45 Minutes
E1 7
0.01
Saarbrücken

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

Jennifer Müller
2900
--email hidden
passcode not visible
logged in users only

Jennifer Müller, 07/16/2013 11:31 -- Created document.