概要

本研究では,定性空間表現 PLCA を定理証明器 Coq を使って形式化し,その平面
性に関する性質を証明する.PLCA はある図形上のオブジェクトの間に成り立つ
性質を記号表現する手法である. 定性空間表現については,これまで多くのシス
テムが提案されているが,それが満たす性質の保証についてほとんど言及されて
いなかった. 本研究では,その1つである PLCA に計算可能なモデルを与える.ま
ず,3 つの構成子を使ってPLCA を帰納的に定義し,結果として得られる PLCA 表
現に対応する 2 次元平面上の図形が存在することを Coq を使って証明する.次
に,対象となる 2 次元平面上の図形が帰納的な PLCA で構築できることの証明
の戦略を与える. 形式化においては,オブジェクト同士の同値類の定義や PLCA
表現の等価性についても定義が必要となり,これらに関する性質も同時に証明す
る.形式化を行うことで PLCA に厳密な定義を与えることができた.証明は帰納
法に基づくものであり,Coq を使用することで証明の正しさが保障される.

発表論文
 
"定性空間表現PLCAのモデル化と妥当性の証明について," 
日本ソフトウェア科学会第30回大会, September, 2013. 

"A Qualitative Representation of a Figure and Construction 
of Its Planar Class," 
Seventh International Conference on Agents and Artificial Intelligence (ICAART15), pp.204-213, January, 2014.

"定性空間表現の Coq による形式化およびその平面性の証明," 
情報処理学会第103回PRO研究会資料, March, 2015.

"Construction of a Planar PLCA Expression: A Qualitative Treatment of Spatial Data," 
Agents and Artificial Intelligence, 7th International Conference, ICAART 2015, Lisbon, Portugal,
January 10-12, 2015, Revised Selected Papers, pp. 298-315, LNAI 9494, Springer-Verlag, 
December, 2015. 

"Towards Verified Construction for Planar Class of a Qualitative Spatial Representation," 
SCSS 2016: 7th International Symposium on Symbolic Computation in Software Science, 
EPiC Series in Computing, Vol.39, pp.117-129, March, 2016.