User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse




Conference Paper

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


Sturm,  Thomas
Automation of Logic, MPI for Informatics, Max Planck Society;

There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available

Lasaruk, A., & Sturm, T. (2011). Automatic Verification of the Adequacy of Models for Families of Geometric Objects. In T. Sturm, & C. Zengler (Eds.), 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
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.