2015 Fiscal Year Annual Research Report
| Project/Area Number |
25330274
|
|---|
| Research Institution | Kwansei Gakuin University |
|---|
Principal Investigator |
高橋 和子 関西学院大学, 理工学部, 教授 (30330400)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
巳波 弘佳 関西学院大学, 理工学部, 教授 (40351738)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | 時空間推論 / 人工知能 / 計算モデル / ソフトウェア工学 / 定性推論 |
|---|
| Outline of Annual Research Achievements |
1. 昨年度作成した，相対的高さ情報をもつ定性表現から 3 次元図形を描画するプログラムを改良し，扱える地形のパターンを増やした．本年度は，これまで扱えなかった傾斜方向の組み合わせを扱えるようにし，さらにこれまでは面として矩形のみを扱っていたのを三角形も扱えるように拡張した．また，定性表現の理解を助けるため，入力インタフェースを作成し，GUI を使った入力から記号表現に自動変換できるようにした．
2. 矩形の重ね合わせに関する推論システムの改良を行った．表示すべき部分と隠す部分が明示された矩形のペアに対して，すべての表示すべき部分を前面に出し，隠す部分はできるだけ背面にくるような重ね合わせ方を推論によって求める矩形推論システムを改良した．これまでに開発された手法ではもれていた解も含めすべての解を効率よく求める方法を考案した．さらに，GUI を使ったシステムとして実装した．
3. 定性空間表現の 1 つ PLCA についてその計算モデルを作成し，無矛盾性や平面性などの性質について証明支援系 Coq を使って表現し証明を行った．机上の証明で見落としていたケースが発見されただけでなく，定義の曖昧性や思い込みによる厳密なモデル化の必要性が判明したため，再度計算モデルを構築した．帰納的に定義された PLCA が無矛盾性や平面性などの性質を満たすことは証明できた．この逆については，一部は Coq で証明し，残りはある補題を仮定することで証明できることを示した．この補題は，証明すべき性質の整楚性にからむものであり，机上では証明可能なものの，ツールによる厳密な証明では場合分けの全容が明確にならず期間中には証明を完成するには至らなかった．
|
