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

Lasaruk, Aless; Sturm, Thomas

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

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 公開

表示: 全項目非表示: 全項目

基本情報

表示: 非表示:

アイテムのパーマリンク: https://hdl.handle.net/11858/00-001M-0000-0010-14E8-D 版のパーマリンク: https://hdl.handle.net/21.11116/0000-000E-33FD-C

資料種別: 会議論文

ファイル

表示: ファイル

作成者

表示:

非表示:

作成者:
Lasaruk, Aless¹, 著者
Sturm, Thomas², 著者

所属:
1External Organizations, ou_persistent22
2Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545

内容説明

表示:

非表示:

キーワード: -

要旨: 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.

資料詳細

表示:

非表示:

言語: eng - English

日付: オンライン出版: 2011出版: 2011

出版の状態: 出版

ページ: -

出版情報: -

目次: -

査読: -

識別子（DOI, ISBNなど）: eDoc: 619018
DOI: 10.1007/978-3-642-21046-4_6
URI: http://www.springerlink.com/content/6n473q44l527qmw7/fulltext.pdf
その他: Local-ID: C125716C0050FB51-6C7DAF04032485E3C1257987003DD415-LasarukSturm:11a

学位: -

訴訟

表示:

Project information

表示:

出版物 1

表示:

非表示:

出版物名: Automated Deduction in Geometry

副タイトル : 7th International Workshop, ADG 2008, Shanghai, China, September 22-24, 2008. Revised Papers

省略形 : ADG 2008

種別: 会議論文集

著者・編者:
Sturm, Thomas¹, 編集者
Zengler, Christoph², 編集者

所属:
1 Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545
2 External Organizations, ou_persistent22

出版社, 出版地: Berlin : Springer

ページ: - 巻号: - 通巻号: - 開始・終了ページ: 116 - 140 識別子（ISBN, ISSN, DOIなど）: ISBN: 978-3-642-21045-7

出版物 2

表示:

非表示:

出版物名: Lecture Notes in Artificial Intelligence

省略形 : LNAI

種別: 連載記事

著者・編者:

所属:

出版社, 出版地: -

ページ: - 巻号: 6301 通巻号: - 開始・終了ページ: - 識別子（ISBN, ISSN, DOIなど）: -

アイテム詳細

基本情報

ファイル

関連URL

作成者

内容説明

資料詳細

関連イベント

訴訟

Project information

出版物 1

出版物 2