# Item

ITEM ACTIONSEXPORT

Released

Conference Paper

#### Automatic Verification of the Adequacy of Models for Families of Geometric Objects

##### Locator

There are no locators available

##### Fulltext (public)

There are no public fulltexts available

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Lasaruk, A., & Sturm, T. (2011). Automatic Verification of the Adequacy of Models
for Families of Geometric Objects. In T. Sturm, & C. Zengler (*Automated
Deduction in Geometry* (pp. 116-140). Berlin: Springer. doi:10.1007/978-3-642-21046-4_6.

Cite as: http://hdl.handle.net/11858/00-001M-0000-0010-14E8-D

##### Abstract

We consider parametric families of semi-algebraic geometric objects, each
implicitly defined by a first-order formula. Given an unambiguous description
of such an object family and an intended alternative description we
automatically construct a first-order formula which is true if and only if our
alternative description uniquely describes geometric objects of the reference
description. We can decide this formula by applying real quantifier
elimination. In the positive case we furthermore derive the defining
first-order formulas corresponding to our new description. In the negative case
we can produce sample points establishing a counterexample for the uniqueness.
We demonstrate our method by automatically proving uniqueness theorems for
characterizations of several geometric primitives and simple complex objects.
Finally, we focus on tori, characterizations of which can be applied in spline
approximation theory with toric segments. Although we cannot yet practically
solve the fundamental open questions in this area within reasonable time and
space, we demonstrate that they can be formulated in our framework. In addition
this points at an interesting and practically relevant challenge problem for
automated deduction in geometry in general.