論証支援のための証明コンストラクタ

概要

論文の詳細を見る
プログラムの作成,検証の他,様々な局面において何らかの対象モデルを構築し,そのモデルを操作することで問題解決を計ることが行われる。そのような対象モデルの表現の手段の1つとして,論理に基づくものが考えられる。我々は論理系に基づくモデルの構築・操作を計算機で支援するための論証支援システムについて研究を行っている。問題領域に応じた論理系を定義し,その論理系の下での論証を支援するためには,その支援システムは論理系の定義機能,およびその論理系の下での証明に対する"編集"機能を持つようなメタ・システムが必要となる。本稿では,このようなメタ・システムへの第一歩として試作している証明の編集システム(証明コンストラクタ)について考察する。このコンストラクタは論理式の入力のためのツールとして,論理式入力編集機能を特に備えている。第2節では本コンストラクタが証明の構成過程をどのようなイメージで捉えているのかについて説明する。第3節では証明コンストラクタの持つ種々の機能について概要を説明する。第4節では論理式入力支援機能について述べる。
一般社団法人情報処理学会の論文
1986-10-01