講演名 2003/5/22
類推機能をもった対話型シークェント計算証明システムの開発(<特集>「自動推論:帰納,演繹,モデル検査/生成,学習,発見,仮説推論,論理プログラム,プランニングetc.」及び一般)(一般及び自動推論)
山田 敬三, 平田 耕一, 原尾 政輝,
PDFダウンロードページ PDFダウンロードページへ
抄録(和) シークェント計算に基づく証明は人間にとって解かりやすく教育支援をはじめ多くの応用が可能である.しかしながら,推論過程が複雑なため自動化は困難である.本橋では,類推機能を導入することによって半自動的に機能する対話型シークェント証明システムの開発をしたので,その概要について述べる.
抄録(英) Since a proof based on sequent calculus is easy to understand for human, it has many applications including computer aided education. However, it is difficult to automate because its inference process is complex. We develop an interactive semi-automated sequent calculus prover by introducing an analogycal reasoning mechanism. In this paper, we demonstrate the outline of our system.
キーワード(和) 類推 / 対話型証明システム / シークェント計算
キーワード(英) analogy / interactive proving system / sequent calculus
資料番号 AI2003-3
発行日

研究会情報
研究会 AI
開催期間 2003/5/22(から1日開催)
開催地(和)
開催地(英)
テーマ(和)
テーマ(英)
委員長氏名(和)
委員長氏名(英)
副委員長氏名(和)
副委員長氏名(英)
幹事氏名(和)
幹事氏名(英)
幹事補佐氏名(和)
幹事補佐氏名(英)

講演論文情報詳細
申込み研究会 Artificial Intelligence and Knowledge-Based Processing (AI)
本文の言語 JPN
タイトル(和) 類推機能をもった対話型シークェント計算証明システムの開発(<特集>「自動推論:帰納,演繹,モデル検査/生成,学習,発見,仮説推論,論理プログラム,プランニングetc.」及び一般)(一般及び自動推論)
サブタイトル(和)
タイトル(英) Developping Interactive Sequent Caliculus Prover Based on Analogy
サブタイトル(和)
キーワード(1)(和/英) 類推 / analogy
キーワード(2)(和/英) 対話型証明システム / interactive proving system
キーワード(3)(和/英) シークェント計算 / sequent calculus
第 1 著者 氏名(和/英) 山田 敬三 / Keizo YAMADA
第 1 著者 所属(和/英) 九州工業大学情報工学部
Faculty of Computer Science and Systems Engineering, Kyushu Institute of Tecnology
第 2 著者 氏名(和/英) 平田 耕一 / Kouichi HIRATA
第 2 著者 所属(和/英) 九州工業大学情報工学部
Faculty of Computer Science and Systems Engineering, Kyushu Institute of Tecnology
第 3 著者 氏名(和/英) 原尾 政輝 / Masateru HARAO
第 3 著者 所属(和/英) 九州工業大学情報工学部
Faculty of Computer Science and Systems Engineering, Kyushu Institute of Tecnology
発表年月日 2003/5/22
資料番号 AI2003-3
巻番号(vol) vol.103
号番号(no) 103
ページ範囲 pp.-
ページ数 4
発行日