de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Conference Paper

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

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons73108

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

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 (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
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.