論証支援システムのための論理式エディタ

概要

論文の詳細を見る
計算機科学や人工知能の分野において,計算機による問題解決やその支援の研究が盛んである.これらを実現する上で,「問題解決とは,把握した問題を適当な公理系の下で形式化し,論証を行うことである」と見做す論理学的方法の有効性が指摘されている.しかし,このような過程の全てを自動的に行うことは非常に難しいため,まず問題の形式化や,論証に必要な論理式の操作を支援するような論証支援システムが望まれる.このような論証支援システムは,既に研究されているが,いずれも特定の論理に対して支援を行うものである.一方,問題を形式化するための論理は問題に応じて多種多様に存在している.これら多種多様な論理の下での論証支援には,それぞれの論理に対して支援システムを構築するのではなく,汎用の論証支援システムを提供することが有効であると考える.また,論証の支援には,問題の形式化,すなわち証明を行うのに必要な論理式の入力,編集の支援と,入力論理式に対する証明の支援の2つが考えられる.本論文では,汎用の論証支援システムにおいて前者の支援を会話的に行うことを目的とする論理式エディタについて報告する.後者の支援に関しては,[4]を参照されたい.なお,本研究は,新世代コンピュータの開発の一環として,ICOTの委託によって行ったものである.
一般社団法人情報処理学会の論文
1986-10-01

論証支援システムのための論理式エディタ

スポンサーリンク

概要

著者

関連論文

スポンサーリンク