| 講演名 | 2002/5/17 証明支援システムxpe(<特集>自動推論 : 演繹, 帰納, モデル検査/生成, 仮説推論アブダクション, 論理プログラム, プランニング, 時相論理, etc.) 毛利 元彦, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 本稿では,証明支援システムとしてのxpeについて説明する.本システムは数理論理学における形式的証明を支援するシステムである.xpeは元々はTEXの証明図マクロproof.styと互換性を持つ証明図作成ソフトであった.TEXのコマンドを解釈・表示し,必要に応じて証明図に論理式の挿入を行うことができる.そして,xpeをユーザーインターフェースとし,xpeから定理自動証明プログラムを呼び出すことで,全体として新しい形の証明支援システムを提供する.xpeを用いることにより証明図の可読性や再利用性が極めて高くなる.xpeはインタラクティブな操作性を持つので,証明途中の証明図を入力し未完成な部分を定理自動証明プログラムにかけることで全体の証明図を得ることも可能である.このように,xpeは定理自動証明を越えた証明支援システムを提供する. |
| 抄録(英) | This paper offers a proof assistant system xpe. It assists formal proof in mathematical logic. It was just a editor with windows system for proof figures on TEX. It has compatibility with proof.sty macros. It interprets and displays TEX commands. You can insert any formula between formulas in a proof figure interactively. We provide a new type proof assistant system `xpe' as a whole, that is used as user interface, and calls theorem prover programs. It has readability, reusability of proof figures. Since it has interactive operativity, we can obtain a complete proof figure if we input a incomplete proof figure and execute a theorem prover program to incomplete parts. Finally xpe is a proof assistant system beyond just a automated reasoning system. |
| キーワード(和) | 定理自動証明 / 証明図 / TEX / エディタ / 証明反駁アルゴリズム |
| キーワード(英) | automated theorem proving / proof figure / TEX / editor / proof or refutation algorithm |
| 資料番号 | AI2002-10 |
| 発行日 |
| 研究会情報 | |
| 研究会 | AI |
|---|---|
| 開催期間 | 2002/5/17(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Artificial Intelligence and Knowledge-Based Processing (AI) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 証明支援システムxpe(<特集>自動推論 : 演繹, 帰納, モデル検査/生成, 仮説推論アブダクション, 論理プログラム, プランニング, 時相論理, etc.) |
| サブタイトル（和） | |
| タイトル（英） | A Proof Asistant System xpe |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 定理自動証明 / automated theorem proving |
| キーワード(2)（和/英） | 証明図 / proof figure |
| キーワード(3)（和/英） | TEX / TEX |
| キーワード(4)（和/英） | エディタ / editor |
| キーワード(5)（和/英） | 証明反駁アルゴリズム / proof or refutation algorithm |
| 第 1 著者 氏名（和/英） | 毛利 元彦 / Motohiko MOURI |
| 第 1 著者 所属（和/英） | 北海道大学工学部知識メディアラボラトリ Meme Media Laboratory, Faculty of Engineering, Hokkaido University |
| 発表年月日 | 2002/5/17 |
| 資料番号 | AI2002-10 |
| 巻番号（vol） | vol.102 |
| 号番号（no） | 91 |
| ページ範囲 | pp.- |
| ページ数 | 5 |
| 発行日 | |