Geometric reasoning with logic and algebra

摘要

Geometric reasoning is concerned with (geometric) objects that often are definable by formulae of the language of the first-order theory of the real numbers. Certain problems that arise in geometric reasoning can be cast into one of the following forms: query problem—does a certain collection of objects possess a certain (first-order) property; constraint problem—given a quantified formula defining an object, find an equivalent definition by a quantifier-free formula; display problem—describe an object, e.g. determine its dimension or specify its topology. In the last fifteen years, feasible algorithms for the exact solution of these problems have been discovered, implemented, and used to solve nontrivial problems. We give examples of problems that fall within the scope of these methods, provide a tutorial introduction to the principal algorithms currently in use, and describe the solution of the sample problems using those algorithms.