Campus Event Calendar
Event Entry
New for: D2, D3
What and Who
Effective Quantifier Elimination - Implementations, Applications, Perspectives
Thomas Sturm
Max-Planck-Institut für Informatik - RG 1
Joint MPI-INF/MPI-SWS Lecture Series
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
MPI Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 4 May 2011
12:15
60 Minutes
E1 4
024
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 to make use of subalgorithms from symbolic computation. The talk
gives an overview of several theories that admit quantifier elimination
and for which there are implementations available in our open-source
software Redlog. The focus is on real quantifier elimination and its
applications and on recent research on quantifier elimination for the
integers. We are also going to consider parametric quantified
SAT-solving as an example for effective quantifier elimination over
initial Boolean algebras.
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 to make use of subalgorithms from symbolic computation. The talk
gives an overview of several theories that admit quantifier elimination
and for which there are implementations available in our open-source
software Redlog. The focus is on real quantifier elimination and its
applications and on recent research on quantifier elimination for the
integers. We are also going to consider parametric quantified
SAT-solving as an example for effective quantifier elimination over
initial Boolean algebras.
Contact
Jennifer Müller
900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 04/27/2011 10:41
Jennifer Müller, 03/30/2011 15:07
Jennifer Müller, 03/29/2011 15:10 -- Created document.
Jennifer Müller, 03/30/2011 15:07
Jennifer Müller, 03/29/2011 15:10 -- Created document.