定性空間表現のCoqによる形式化およびその平面性の証明

• Item type: Trans(1)
• 公開日: 2015-09-21
• タイトル: 定性空間表現のCoqによる形式化およびその平面性の証明
• タイトル / 言語: en
• タイトル: Formalization of a Qualitative Spatial Representation and the Proof for Its Planarity Using Coq
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [発表概要]
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 関西学院大学理工学部情報科学科
• 著者所属: 関西学院大学理工学部情報科学科
• 著者所属: 関西学院大学理工学部情報科学科
• 著者所属(英): en
• 著者所属(英): School of Science and Technology, Kwansei Gakuin University
• 著者所属(英): en
• 著者所属(英): School of Science and Technology, Kwansei Gakuin University
• 著者所属(英): en
• 著者所属(英): School of Science and Technology, Kwansei Gakuin University
• 著者名: 後藤, 瑞貴; 森口, 草介; 高橋, 和子
• 著者名(英): Mizuki, Goto; Sousuke, Moriguchi; Kazuko, Takahashi
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 定性空間表現PLCAを帰納的に定義することでモデル化し，このモデルの集合が平面性を満たすPLCAの集合と一致していることを，証明支援系Coqを用いて証明する．PLCAは，空間データに対して，それを構成する点（Point），線（Line），周（Circuit），範囲（Area）というオブジェクトを用いそれらの包含関係によってそれを表現する手法である．この表現は座標データを用いずに領域同士の接続関係を定性的に表すもので，空間データ上に関して焦点をしぼった推論ができる．推論の正当性を保証するためには，PLCAと空間データの対応関係を証明する必要があるが，与えられたPLCA表現が二次元平面に埋め込めるための条件は示されているものの，平面性を満たすPLCAの集合を帰納的に構築する方法については議論されていない．本発表では，まず，3つの構成子を用いてPLCAを帰納的に定義し，これらによって構築されるモデルが平面性条件を満たすことを証明する．証明は，帰納法に基づき，各構成子に対して場合分けして行う．また，平面性条件を満たすPLCAと表現上等価な帰納的PLCAが構築できることを範囲の数に関する帰納法を使って証明する．証明では，範囲の数を増やしたときのPLCAの型を平面性条件から得られるものと一致させる必要があり，帰納の仮定となるPLCAを適切に設定することで証明の道筋を得ることができた．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: We give a model to a qualitative spatial representation PLCA by formalizing it inductively, and prove that such a model coincides with the planar PLCA, using a proof assistant Coq. PLCA provides a symbolic expression of spatial entities and allows reasoning on this expression. To justify the reasoning, we should prove the correspondence between PLCA expression and spatial data; for a given PLCA expression, the conditions for planarity have been shown, but the construction of such a PLCA expression has not been discussed. In this presentation, we give an inductive definition to PLCA with three constructors, and prove that the obtained model satisfies the conditions for planarity. The proof is based on induction and using case split on each constructor. On the other hand, we prove that an inductive PLCA can be constructed that is equivalent to a planar PLCA expression, using an induction on the number of areas. In the proof, we should match the type of PLCA with the succeeding number of the areas with that obtained by the conditions for planarity. Taking an appropriate PLCA as an induction hypothesis has solved this problem and guided us to get the proof.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 8, 号 3, p. 36-36, 発行日 2015-09-21
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会