Computer Science Logic and 8th Kurt Gödel Colloquium
Nicolai Vorobjov: Effective quantifier elimination over real closed fields
Welcome and News
Host Institutions
Calls and Deadlines
Program
Social Program
Registration
Location and Venue
Accommodation
Committees
Contact
Colocated Events
Authors' instructions
Print current pagePrint this page
In early 30s A. Tarski, motivated by a problem of automatic theorem proving in elementary algebra and geometry, suggested an algorithm for quantifier elimination in the first order theory of the reals. The complexity of Tarski's algorithm is a non-elementary function of the format of the input formula.

In mid-70s a group of algorithms appeared based on the idea of a cylindrical cell decomposition and having an elementary albeit doubly-exponential complexity, even for deciding closed existential formulae. The tutorial will explain some ideas behind a new generation of algorithms which were designed during 80s and 90s and have, in a certain sense, optimal (singly-exponential) complexity.

In a useful particular case of closed existential formulae (i.e., deciding feasibility of systems of polynomial equations and inequalities) these new algorithms are theoretically superior to procedures known before in numerical analysis and computer algebra.

© 2002-2003 Kurt Gödel Society, Norbert Preining. 2003-07-09 Valid HTML 4.01! Valid CSS! Debian