Quantifier elimination and cylindrical algebraic decomposition. Proceedings of a symposium, Linz, Austria, October 6--8, 1993
type: Item
instance of: scholarly article
title: Quantifier elimination and cylindrical algebraic decomposition. Proceedings of a symposium, Linz, Austria, October 6--8, 1993
zbMATH Open document ID: 0906.03033
published in: Texts \& Monographs in Symbolic Computation
publication date: 1997-06-02T00:00:00Z
review text: The articles of this volume will be reviewed individually. The book contains the contributions of the participants of the symposium on quantifier elemination and cylindrical algebraic decomposition, which was held in Linz (Austria) during October 1993. The Cylindrical Algebraic Decomposition (CAD) is a method of eliminating quantifiers in the language of real arithmetic. This language contains symbols for addition, multiplication and inequality in the reals, together with symbols for 0 and 1. The formulas of the language are built from these symbols, the usual quantifiers -- existential and universal -- and parenthesis; in the usual way one builds `meaningful' formulas in mathematics. Any algorithm for eliminating quantifiers, such as CAD, inputs such a formula and outputs an equivalent formula without quantifiers. It was first demonstrated by Tarski, in 1930, that such an algorithm exists. It is clear that a quantifier-free equivalent of a formula is easy to handle -- algorithmically and mathematically; if the initial formula was a sentence, then the quantifier-free equivalent is a Boolean combination of equations and inequalities among constants (rational numbers) which is either true -- if the sentence was true -- or false. In such a way one can verify or reject algorithmically guessed `possible theorems'. In general the quantifier-free equivalent of a formula reveals the mathematical content of the original formula in a way easily to handle. The main problem with such algorithms is their time complexity. The worst case complexity of the original algorithm of Tarski is given by a stack of exponentials whose size depends on the number of quantifiers. Collins, the inventor of CAD, has given a doubly exponential -- in the number of variables -- time complexity for his algorithm; Davenport, Heintz and recently Weispfenning have given doubly exponential lower bounds, even for simple formulas such as linear ones. The intrinsic hardness of the problem calls for study of…
Mathematics Subject Classification ID: 03C10
Mathematics Subject Classification ID: 68W30
Mathematics Subject Classification ID: 00B25
Mathematics Subject Classification ID: 03-06
zbMATH DE Number: 1016340
zbMATH Keywords: Quantifier elimination
zbMATH Keywords: Cylindrical algebraic decomposition
zbMATH Keywords: Symposium
zbMATH Keywords: Proceedings
zbMATH Keywords: Linz (Austria)
zbMATH Keywords: quantifier elemination
zbMATH Keywords: cylindrical algebraic decomposition
zbMATH Keywords: language of real arithmetic
reviewed by: Thanases Pheidas
MaRDI profile type: Publication
description: scientific article; zbMATH DE number 1016340