Quantifier Elimination

Description
Recently, quantifier elimination algorithms have seen many applications, and there have been new development in quantifier elimination algorithms for special classes of problems.

Titles

2. Simple Solution Formula Construction from Truth Invariant CADs
   
3. REDLOG -- Computer Algebra Meets Computer Logic
   
4. Approximate Quantifier Elimination
5. Quantifier Elimination Applied in Simulation and Scheduling
   
6. Some Applications of Quantifier Elimination in Nonlinear Control Theory
   
7. On the Determination of the Strong Stabilizability of an n-Dimensional Linear System
   
8. The Stability of Boundary Conditions
   
9. Discussion and Comments by the Organizers and Participants

   1. Christopher W. Brown         cbrown@jade.risc.uni-linz.ac.at
   2. George Collins               George.Collins@risc.uni-linz.ac.at
   3. Emma-Neila Gonzalez-Campos   gcampos@matsun1.unican.es
   4. Andreas Dolzmann             Andreas.Dolzmann@fmi.uni-passau.de
   5. Hoon Hong                    hhong@risc.uni-linz.ac.at
   6. Mats Jirstrand               matsj@isy.liu.se
   7. Ying Jiangqian               ying@ikd.info.gifu-u.ac.jp
   8. Richard Liska                liska@siduri.fjfi.cvut.cz
   9. Andreas Neubacher            aneubach@risc.uni-linz.ac.at
  10. Stanly Steinberg             stanly@math.unm.edu
  11. Thomas Sturm                 sturm@fmi.uni-passau.de
  12. Lalo Gonzales Vega           gvega@matsun1.unican.es
  13. Volker Weispfenning          weispfen@alice.fmi.uni-passau.de

• REDLOG -- Computer Algebra Meets Computer Logic
  Andreas Dolzmann and Thomas Sturm
  Abstract REDLOG is a package that extends the computer algebra system reduce to a computer logic system, i.e., a system that provides algorithms for the symbolic manipulation of first-order formulas over some temporarily fixed language and theory. In contrast to theorem provers, the methods applied know about the underlying algebraic theory and make use of it. Though the focus is on simplification, parametric linear optimization, and quantifier elimination, REDLOG is designed as a general-purpose system. It has been applied successfully for solving non-academic problems, mainly for the simulation of networks. We describe the functionality of REDLOG as it appears to the user, and explain the design issues and implementation techniques.

• Quantifier Elimination Applied in Simulation and Scheduling
  Volker Weispfenning
  Abstract

• Global projection operators for the Cylindrical Algebraic Decomposition algorithm
  Emma-Neila Gonzalez-Campos and Laureano Gonzalez-Vega
  Abstract: The projection phase in the CAD algorithm proceeds by eliminating one variable on a given set of polynomials X via the computation of the principal subresultant coefficients of a well precised set of polynomials pairs on X (including their derivatives and their reductums). Since the size, at least in number, of this new set of polynomials is usually very big, any improvement in the projection phase would convey to dramatically speed up the efficiency of the CAD algorithm. The purpose of this talk is to present two approaches allowing, in some cases, to simplify the projection phase in the CAD algorithm:
  -. The first one tries to avoid the consideration of all the different pairs of polynomials and their reductums by parametrizing the rank of a well precised matrix with polynomial entries.
  -. The second one tries to perform an improved projection phase through the elimination of blocks of variables instead of the usual one by one variable elimination.
  The theoretical tools to be used include Barnett's Theorem characterizing the degree of the gcd of a finite set of polynomials through the rank of a well-precised matrix and the parametrization of Hermite's Method for counting the number of real solutions of a polynomial system of equations.

• Simple Solution Formula Construction from Truth Invariant CADs
  Chris Brown and George Collins
  Abstract

• Some Applications of Quantifier Elimination in Nonlinear Control Theory
  Mats Jirstrand
  Abstract: Many problems in control theory can be formulated as formulas in the first order theory of real closed fields. In this talk we investigate some of the expressive power of this theory. We consider dynamical systems described by polynomial differential equations subjected to constraints on control and system variables and show how to formulate questions in the above framework which can be answered by quantifier elimination. The treated problems regards stationarity, stability, and tracking of a polynomially parameterized curve. The software package QEPCAD has been used to perform quantifier elimination in a number of examples.

• On the Determination of the Strong Stabilizability of an n-Dimensional Linear System
  Ying Jiangqian
  Dept. Electronics and Computer Engineering
  Gifu University, Yanagido, Gifu, 501, Japan
  Abstract: An n-dimensional linear system described by a rational transfer function is stable by definition if the function is free from 0 on the n-D polydisc in the complex space. A system is said to be strongly stabilizable if there exists a stable compensator that makes the system stable. A topological condition was recently derived by Shiva Shankar[1] to determine whether a system can can be strongly stabilized or not. In this talk we show that in certain restricted case this topological condition can be reduced to a geometrical one and can be solved based the cylindrical algebraic decomposition of complex algebraic variety.
  [1] Shiva Shankar, An Obstruction to the Simultaneous Stabilization of Two n-D plants, Acta Applicandae Mathematicae 36:289-301,1994

• Approximate Quantifier Elimination
  H. Hong and A. Neubacher
  Abstract To be supplied.

• The Stability of Boundary Conditions
  R. Liska and S. Steinberg
  Abstract: The question of whether boundary conditions in an initial-boundary value problem for a partial differential equation or for a finite-difference equation are stable or not can be reduced to a quantifier elimination problem with many equalities. This talk will show how to do the reduction and explore some techniques for solving such problems.

  Such stability problems are critical part of developing stable boundary conditions for higher-order discretizations of partial differential equations.

• Discussion and Comments by the Organizers and Participants
  H. Hong, R. Liska, S. Steinberg
  Abstract: The organizers will make some summary comments and then begin a discussion session.