Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:




Library Locked Library locked




Author, Editor

Author(s):

Lasaruk, Aless
Sturm, Thomas

dblp
dblp

Not MPG Author(s):

Lasaruk, Aless

Editor(s):

Sturm, Thomas
Zengler, Christoph

dblp
dblp

Not MPII Editor(s):

Zengler, Christoph

BibTeX cite key*:

LasarukSturm:11a

Title, Booktitle

Title*:

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

Booktitle*:

Automated Deduction in Geometry : 7th International Workshop, ADG 2008

Event, URLs

URL of the conference:

http://adg2008.redlog.eu/

URL for downloading the paper:

http://www.springerlink.com/content/6n473q44l527qmw7/fulltext.pdf

Event Address*:

Shanghai, China

Language:

English

Event Date*
(no longer used):


Organization:


Event Start Date:

22 September 2008

Event End Date:

24 September 2008

Publisher

Name*:

Springer

URL:

http://www.springer.com

Address*:

Berlin

Type:


Vol, No, Year, pp.

Series:

Lecture Notes in Artificial Intelligence

Volume:

6301

Number:


Month:

May

Pages:

116-140

Year*:

2011

VG Wort Pages:

43

ISBN/ISSN:

978-3-642-21045-7

Sequence Number:


DOI:

10.1007/978-3-642-21046-4_6



Note, Abstract, ©


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

URL for the Abstract:

http://www.springerlink.com/content/6n473q44l527qmw7

Keywords:

Real Geometry, Unique Representation, Automated Proving, Real Quantifier Elimination



Download
Access Level:

Public

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Automation of Logic

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:

@INPROCEEDINGS{LasarukSturm:11a,
AUTHOR = {Lasaruk, Aless and Sturm, Thomas},
EDITOR = {Sturm, Thomas and Zengler, Christoph},
TITLE = {Automatic Verification of the Adequacy of Models for Families of Geometric Objects},
BOOKTITLE = {Automated Deduction in Geometry : 7th International Workshop, ADG 2008},
PUBLISHER = {Springer},
YEAR = {2011},
VOLUME = {6301},
PAGES = {116--140},
SERIES = {Lecture Notes in Artificial Intelligence},
ADDRESS = {Shanghai, China},
MONTH = {May},
ISBN = {978-3-642-21045-7},
DOI = {10.1007/978-3-642-21046-4_6},
}


Entry last modified by Anja Becker, 03/16/2012
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
[Library]
Created
01/16/2012 12:15:19 PM
Revisions
2.
1.
0.

Editor(s)
Anja Becker
Thomas Sturm
Thomas Sturm

Edit Dates
16.03.2012 14:20:33
01/16/2012 12:36:26 PM
01/16/2012 12:15:19 PM

Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section