1995 Fiscal Year Annual Research Report
| Project/Area Number |
07680380
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
坂井 公 筑波大学, 数学系, 助教授 (20241797)
|
|---|
| Keywords | 証明検証 / 型理論 / 等式論理 / 高階単一化 / 等式公理下での単一化 |
|---|
| Research Abstract |
本研究の目的は計算機に人間の行なう数学的思考の一部を補佐・代行させる可能性を探ることであった。特に等式に関わる推論機能の強化を図るために、次のような調査・検討・試作などを行った。
・高階の型理論や等式論理を応用した証明検証方式やそれに基づく知的計算機システムの正当性、有効性、効率などについて文献などを参照しながら、理論的に検討した。
・上の理論に基づいて作成されたいくつかの既存システムの仕組みや使用感について調査した。この調査は、主に文献調査により、一部は、実際に試用してみることで行った。
・この種のシステムを構築する上での中核技術となるものが高階単一化アルゴリズムがや等式公理下の単一化アルゴリズムなどであることは明らかなので、これらについて文献などから最近の研究動向、技術動向を調査した。
・高階単一化、等式公理下の単一化ともに多くのアルゴリズムの提案があるが、そのうち特に有望そうなものについて、試作的インプリメントに着手した。
・試作と同時にアルゴリズムの効率改善や機能拡張について調査を進め、また独自の手法による改善検討を始めた。
上記の第4項、第5項については、十分に時間が取れなかったために、不満の残る結果となっているが、今後、鋭意研究を進めて行くつもりである。
|
