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

後藤 瑞貴; 森口 草介; 高橋 和子

論文・著書情報

タイトル

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

著者

和文:	後藤瑞貴, 森口草介, 高橋和子.
英文:	後藤瑞貴, Sosuke Moriguchi, 高橋和子.

言語

Japanese

掲載誌/書名

和文:	情報処理学会論文誌プログラミング（PRO）
英文:

巻, 号, ページ

Vol. 8 No. 3 pp. 36-36

出版年月

2015年8月

出版者

和文:
英文:

会議名称

和文:
英文:

開催地

和文:
英文:

アブストラクト

定性空間表現PLCAを帰納的に定義することでモデル化し，このモデルの集合が平面性を満たすPLCAの集合と一致していることを，証明支援系Coqを用いて証明する．PLCAは，空間データに対して，それを構成する点（Point），線（Line），周（Circuit），範囲（Area）というオブジェクトを用いそれらの包含関係によってそれを表現する手法である．この表現は座標データを用いずに領域同士の接続関係を定性的に表すもので，空間データ上に関して焦点をしぼった推論ができる．推論の正当性を保証するためには，PLCAと空間データの対応関係を証明する必要があるが，与えられたPLCA表現が二次元平面に埋め込めるための条件は示されているものの，平面性を満たすPLCAの集合を帰納的に構築する方法については議論されていない．本発表では，まず，3つの構成子を用いてPLCAを帰納的に定義し，これらによって構築されるモデルが平面性条件を満たすことを証明する．証明は，帰納法に基づき，各構成子に対して場合分けして行う．また，平面性条件を満たすPLCAと表現上等価な帰納的PLCAが構築できることを範囲の数に関する帰納法を使って証明する．証明では，範囲の数を増やしたときのPLCAの型を平面性条件から得られるものと一致させる必要があり，帰納の仮定となるPLCAを適切に設定することで証明の道筋を得ることができた．

Home

各種検索

サポート

T2R2について

関連リンク

論文・著書情報