English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

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

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.

Item is

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Lasaruk, Aless1, Author
Sturm, Thomas2, Author           
Affiliations:
1External Organizations, ou_persistent22              
2Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Content

show
hide
Free keywords: -
 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.

Details

show
hide
Language(s): eng - English
 Dates: 20112011
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 619018
DOI: 10.1007/978-3-642-21046-4_6
URI: http://www.springerlink.com/content/6n473q44l527qmw7/fulltext.pdf
Other: Local-ID: C125716C0050FB51-6C7DAF04032485E3C1257987003DD415-LasarukSturm:11a
 Degree: -

Event

show
hide
Title: 7th International Workshop on Automated Deduction in Geometry
Place of Event: Shanghai, China
Start-/End Date: 2008-09-22 - 2008-09-24

Legal Case

show

Project information

show

Source 1

show
hide
Title: Automated Deduction in Geometry
  Subtitle : 7th International Workshop, ADG 2008, Shanghai, China, September 22-24, 2008. Revised Papers
  Abbreviation : ADG 2008
Source Genre: Proceedings
 Creator(s):
Sturm, Thomas1, Editor           
Zengler, Christoph2, Editor
Affiliations:
1 Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545            
2 External Organizations, ou_persistent22            
Publ. Info: Berlin : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 116 - 140 Identifier: ISBN: 978-3-642-21045-7

Source 2

show
hide
Title: Lecture Notes in Artificial Intelligence
  Abbreviation : LNAI
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 6301 Sequence Number: - Start / End Page: - Identifier: -