| 研究課題/領域番号 |
25280078
|
|---|
| 研究種目 |
基盤研究(B)
|
| 研究機関 | 北海道大学 |
|---|
研究代表者 |
赤間 清 北海道大学, 情報基盤センター, 特任教授 (50126265)
|
|---|
| 研究分担者 |
荒木 健治 北海道大学, 情報科学研究科, 教授 (50202742)
三浦 克宜 北見工業大学, 工学部, 講師 (50636587)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| キーワード | セマンテックＷｅｂ / 求解問題 / 等価変換 / 関数変数 |
|---|
| 研究概要 |
（A) 一階述語論理式で書かれた求解問題を拡張された節集合に変換するプログラムを構築した。論理式の意味を正確に保存する「意味保存スコーレム化」の理論を与え、それに基づいて、アルゴリズムを設計した。その結果、与えられた求解問題は、「funcアトムという特別なアトムを含む拡張された節空間」に写像され、スコーレム化における意味保存が可能となる。これは、計算全体を等価変換にできるためのキーポイントであり、従来研究の限界を超えるために必須の技術である。
(B) アンフォールド変換などの基本変換が利用できる、インタラクテブな等価変換システムを構築し、求解問題の解法を実験的に研究した。そして、いくつかの有用な等価変換ルールを発見した。
(C) ＳＡＴソルバーによる計算を等価変換による計算の１つとして位置付ける理論を開発した。これは、高レベル言語で書かれた求解問題を全自動で高速に解くための要素技術となる。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
求解問題を解くための全体像が明確化できた。拡張された節空間への変換や、拡張された節空間での等価変換の実験を行うことにより、多様な問題を自動的に解くための新たな研究段階に進むことができた。ＳＡＴなどの低レベル計算との関係も解明され、高速解法の開発への見通しが得られた。
|
| 今後の研究の推進方策 |
初年度の研究で、求解問題を解くための基本構造がしだいに明らかになってきた。現実の世界に出現する多くの求解問題を全自動で解く技術を確立することを次の主要な課題とすべきである。そのために、より多くの例題をインタラクテブに解くことを試み、その過程で新たな等価変換ルールを蓄積し、その正当性を証明する。また、解法の自動化を推進するために、等価変換の制御の方法を開発する。高速化の技術としては、ＳＡＴソルバーなどとの連携技術を確立する。
|
| 次年度の研究費の使用計画 |
研究の重心が理論開発であったことと、プログラム要員の雇用をしないで、自前でプログラム開発を行ったことが主な理由である。
未使用額については、次年度の国際会議登録費用や旅費に充てる。
|
