Try Firefox!

Abstracts for Submitted and Published Papers

CHRISTOPHER W. BROWN

Department of Computer Science, United States Naval Academy

[8]
The Complexity of Quantifier Elimination and Cylindrical Algebraic Decomposition This paper has two parts. In the first part we give a simple and constructive proof that quantifier elimination in real algebra is doubly exponential, even when there is only one free variable and all polynomials in the quantified input are linear. The general result is not new, but we hope the simple and explicit nature of the proof makes it interesting. The second part of the paper uses the construction of the first part to prove some results on the effects of projection order on CAD construction -- roughly that there are CAD construction problems for which one order produces a constant number of cells and another produces a doubly exponential number of cells, and that there are problems for which all orders produce a doubly exponential number of cells. The second of these results implies that there is a true singly vs. doubly exponential gap between the worst-case running times of several modern quantifier elimination algorithms and CAD-based quantifier elimination when the number of quantifier alternations is constant.

[12]
RegeXeX: an interactive system providing regular expression exercises This paper presents RegeXeX (Regular expression exercises), an interactive system for teaching students to write regular expressions. The system poses problems (prose descriptions of languages), students enter solutions (regular expressions defining these languages), and the system provides feedback. What is novel in this system is the type of feedback: students are not merely told that a submitted regular expression is wrong, they are given examples of strings that the expression either matches and shouldn't or does not match and should, and asked to try again. Additionally, student responses need only be equivalent to the solution, not identical. Results of classroom experience with this system are also reported, and demonstrate its effectiveness in teaching students to write regular expressions with little or no instructor interaction.

RegeXeX is a freely available, portable system, written in C++ and using the Qt library for its GUI. It is distributed with several exercise sets, but is designed so instructors can easily write their own. The system logs student work and offers facilities for submitting log-files to instructors as well, allowing for automatic grading, or in-depth analysis of student performance and evolution of responses throughout the exercise set.

[11]
Efficient Preprocessing Methods for Quantifier Elimination. Methods for computing formulas equivalent to quantified input formulas based on linear substitution, factorization and AI techniques are discussed within this paper. We present an algorithm for building a search tree consisting of nodes representing equivalent formulas to an input formula, grading these formulas and efficient methods to speed up the computation. We present examples of quantified formulas which can be reduced by our preprocessing method to problems solvable by current quantifier elimination packages, whereas the original formulas had been inaccessible to those.

[10]
Algorithmic Methods for Investigating Equilibria in Epidemic Modelling he calculation of threshold conditions for models of infectious diseases is of central importance for developing vaccination policies. These models are often coupled systems of ordinary differential equations, in which case the computation of threshold conditions can be reduced to the question of stability of the disease-free equilibrium. This paper shows how computing threshold conditions for such models can be done fully algorithmically using quantifier elimination for real closed fields and related simplification methods for quantifier-free formulas. Using efficient quantifier elimination techniques for special cases that have been developed by Weispfenning and others, we can can also compute whether there are ranges of parameters for which sub-threshold endemic equilibria exist.

[13]
On using bi-equational constraints in CAD construction This paper introduces an improved method for constructing cylindrical algebraic decompositions (CADs) for formulas with two polynomial equations as implied constraints. The fundamental idea is that neither of the varieties of the two polynomials is actually represented by the CAD the method produces, only the variety defined by their common zeros is represented. This allows for a substantially smaller projection factor set, and for a CAD with many fewer cells.

In the current theory of CADs, the fundamental object is to decompose n-space into regions in which a polynomial equation is either identically true or identically false. With many polynomials, one seeks a decomposition into regions in which each polynomial equation is identically true or false independently. The results presented here are intended to be the first step in establishing a theory of CADs in which systems of equations are fundamental objects, so that given a system we seek a decomposition into regions in which the system is identically true or false -- which means each equation is no longer considered independently. Quantifier elimination problems of this form (systems of equations with side conditions) are quite common, and this approach has the potential to bring large problems of this type into the scope of what can be solved in practice. The special case of formulas containing two polynomial equations as constraints is an important one, but this work is also intended to be extended in the future to the more general case.

[9]
Algorithmic Methods for Computing Threshold Conditions in Epidemic Modelling The calculation of threshold conditions for models of infectious diseases is of central importance for developing vaccination policies. Frequently coupled systems of ordinary differential equations are used as models and the computation of threshold conditions can be reduced to the question of stability of the disease free equilibrium. We show how the computations of threshold conditions for such models can be done fully algorithmically by using techniques of quantifier elimination for real closed fields and related simplification methods for quantifier-free formulas.

[7]
QEPCAD B - a program for computing with semi-algebraic sets using CAD
This report introduces QEPCAD B, a program for computing with real algebraic sets using cylindrical algebraic decomposition (CAD). QEPCAD B both extends and improves upon the QEPCAD system for quantifier elimination by partial cylindrical algebraic decomposition written by Hoon Hong in the early 1990s. This paper briefly discusses some of the improvements in the implementation of CAD and quantifier elimination via CAD, and provides somewhat more detail on extensions to the system that go beyond quantifier elimination. The author is responsible for most of the extended features of QEPCAD B, but improvements to the basic CAD implementation and to the SACLIB library on which QEPCAD is based are the results of many people's work, including: George E. Collins, Mark J. Encarnación, Hoon Hong, Jeremy Johnson, Werner Krandick, Richard Liska, Scott McCallum, Nicolas Robidoux, and Stanly Steinberg. Source code, documentation and installation instructions for QEPCAD B are all available at www.cs.usna.edu/~qepcad.

[6]
An Overview of QEPCADB: a Tool for Real Quantifier Elimination and Formula Simplification
This paper describes the basic functionality of QEPCAD B, a system for computing with semi-algebraic sets via Cylindrical Algebraic Decomposition (CAD). QEPCAD B is an interactive command-line based program, written in C, and built on top of the SACLIB library. It extends and improves the QEPCAD system. The article focuses on using QEPCAD B to solve problems, describing the basic facilities offered by the system and providing examples of applications of these facilities. The program is freely available at www.cs.usna.edu/~qepcad. Download paper as gzipped postscript file

[4]
Improved Projection for Cylindrical Algebraic Decomposition
McCallum's projection operator for Cylindrical Algebraic Decomposition (CAD) represented a huge step forward for the practical utility of the CAD algorithm. This paper presents a simple theorem showing that the mathematics in McCallum's paper actually point to a better projection operator than he proposes -- a reduced McCallum projection. The reduced projection has the potential to not simply speed up CAD computation for problems that are currently solvable in practice, but actually increase the scope of problems that can realistically be attacked via CAD's. Additionally, the same methods are used to show that McCallum's projection can be reduced still further when CAD is applied to certain types of commonly occurring quantifier elimination problems. Download paper as pdf This material has been published in Journal of Symbolic Computation, 32(5):447-465, November 2001, the only definitive repository of the content that has been certified and accepted after peer review. Copyright and all rights therein are retained by Academic Press. This material may not be copied or reposted without explicit permission.

[5]
Simple CAD Construction and its Applications
This paper presents a method for the simplification of truth-invariant cylindrical algebraic decompositions (CAD's). Examples are given that demonstrate the usefulness of the method in speeding up the solution formula construction phase of the CAD-based quantifier elimination algorithm. Applications of the method to the construction of truth-invariant CAD's for very large quantifier-free formulas and quantifier elimination of non-prenex formulas are also discussed. Download paper as pdf This material has been published in Journal of Symbolic Computation, 31(5):521-547, May 2001, the only definitive repository of the content that has been certified and accepted after peer review. Copyright and all rights therein are retained by Academic Press. This material may not be copied or reposted without explicit permission.

[3]
Improved Projection for CAD's of R3
This paper presents an improved projection operator for the construction of CAD's of R3. It is shown that, typically, it suffices to include in projection only leading coefficients (along with discriminants and resultants) rather than all coefficients. Cases in which the leading coefficient alone does not suffice can be dealt with, in a sense, even more efficiently. Generalizing the improved projection operator to dimension greater than three is a topic of ongoing research.

[2]
Guaranteed Solution Formula Construction
Quantifier elimination transforms a description of a semi-algebraic set as a formula with quantified variables into a description of the set as a quantifier-free formula. Quantifier elimination by cylindrical algebraic decomposition (CAD) does this via an intermediate representation of the semi-algebraic set as a CAD. A quantifier-free formula representation of the set is then constructed from this CAD.

One desirable property of the CAD-based quantifier elimination algorithm is its ability to produce simple solution formulas via methods such as that of [18]. These methods require that the CAD produced as an intermediate representation be projection-definable, which is not the case for all quantifier-elimination problems. This paper presents an efficient method for transforming an arbitrary CAD into a projection-definable CAD, thereby rendering simple solution formula construction methods applicable to all quantifier elimination problems.

[1]
Simplification of Truth-Invariant Cylindrical Algebraic Decompositions
This paper presents a method for simplifying the truth-invariant cylindrical algebraic decomposition (CAD) produced by the stack construction phase of the CAD-based quantifier elimination algorithm. Using this simplified CAD as input to the solution formula construction phase of the algorithm can considerably reduce the complexity of constructing a simple equivalent quantifier-free formula. Other applications requiring a truth-invariant CAD for a formula can also benefit from a simpler CAD. The method is applicable to the decompositions produced by both Collins' original CAD-based quantifier elimination algorithm [15] and Hong's partial-CAD-based algorithm [17,16].

Bibliography

1
C. W. Brown.
Simplification of truth-invariant cylindrical algebraic decompositions.
In Proc. International Symposium on Symbolic and Algebraic Computation, pages 295-301, 1998.

2
C. W. Brown.
Guaranteed solution formula construction.
In Proc. International Symposium on Symbolic and Algebraic Computation, pages 137-144, 1999.

3
C. W. Brown.
Improved projection for CAD's of $\mathbb {R}^3$.
In Proc. International Symposium on Symbolic and Algebraic Computation, pages 48-53, 2000.

4
C. W. Brown.
Improved projection for cylindrical algebraic decomposition.
Journal of Symbolic Computation, 32(5):447-465, November 2001.

5
C. W. Brown.
Simple CAD construction and its applications.
Journal of Symbolic Computation, 31(5):521-547, May 2001.

6
C. W. Brown.
An overview of QEPCAD B: a tool for real quantifier elimination and formula simplification.
Journal of Japan Society for Symbolic and Algebraic Computation, 10(1):13-22, 2003.

7
C. W. Brown.
QEPCAD B - a program for computing with semi-algebraic sets using CADs.
ACM SIGSAM Bulletin, 37(4):97-108, December 2003.

8
Christopher W. Brown and James H. Davenport.
The complexity of quantifier elimination and cylindrical algebraic decomposition.
In ISSAC '07: Proceedings of the 2007 international symposium on Symbolic and algebraic computation, 2007.
To Appear.

9
Christopher W. Brown, M'hammed El Kahoui, Dominik Novotni, and Andreas Weber.
Algorithmic methods for computing threshold conditions in epidemic modelling.
In V. G. Ganzha, E. W. Mayr, and E. V. Vorozhtsov, editors, Computer Algebra in Scientific Computing (CASC '04), pages 51-60, St. Petersburg, Russia, July 2004.

10
Christopher W. Brown, M'hammed El Kahoui, Dominik Novotni, and Andreas Weber.
Algorithmic methods for investigating equilibria in epidemic modelling.
Journal of Symbolic Computation, 41(11):1157-1173, November 2006.

11
Christopher W. Brown and Christian Gross.
Efficient preprocessing methods for quantifier elimination.
In CASC, pages 89-100, 2006.

12
Christopher W. Brown and Eric A. Hardisty.
Regexex: an interactive system providing regular expression exercises.
In Proceedinds of the 38th SIGCSE technical symposium on Computer science education, pages 445-449, New York, NY, USA, 2007. ACM Press.

13
Christopher W. Brown and Scott McCallum.
On using bi-equational constraints in cad construction.
In ISSAC '05: Proceedings of the 2005 international symposium on Symbolic and algebraic comp utation, pages 76-83, New York, NY, USA, 2005. ACM Press.

14
B.F. Caviness and J. R. Johnson, editors.
Quantifier Elimination and Cylindrical Algebraic Decomposition.
Texts and Monographs in Symbolic Computation. Springer-Verlag, 1998.

15
G. E. Collins.
Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition.
In Lecture Notes In Computer Science, volume Vol. 33, pages 134-183. Springer-Verlag, Berlin, 1975.
Reprinted in [14].

16
G. E. Collins and H. Hong.
Partial cylindrical algebraic decomposition for quantifier elimination.
Journal of Symbolic Computation, 12(3):299-328, Sep 1991.

17
H. Hong.
Improvements in CAD-based Quantifier Elimination.
PhD thesis, The Ohio State University, 1990.

18
H. Hong.
Simple solution formula construction in cylindrical algebraic decomposition based quantifier elimination.
In Proc. International Symposium on Symbolic and Algebraic Computation, pages 177-188, 1992.


Christopher W Brown 2007-04-23