（２８）論証支援システム：ＥＵＯＤＨＩＬＯＳ


	マ シ ン：PSI
	環　　境：SIMPOS
	言　　語：ESP
	ソース量：1.7 MB
	文　　書：マニュアル (日本語／英語)

概要

単一の論理に固定されることなく、様々な論理が扱える汎用の論証支援システムである。

特徴

EUODHILOSは様々な論理を扱うための汎用の枠組みを持つことを特徴とする論証支援システムである。そのため、論理系を記述する枠組、記述された論理系上の証明の構築を支援する思考シートと呼ばれる枠組を備えている。論理系記述の中には、どのような論理表現を用いるのかを容易に記述するための構文記述が含まれる。また、規則として推論規則と書き換え規則の両方が自然演繹法スタイルで定義できるため、様々なタイプの論理記述、取り扱いが可能である。

機能

フォント・エディタ、ソフトウェア・キーボードによる論理演算子等の特殊文字の使用が可能。
拡張された DCG (確定節文法) と構成子記述による論理表現構文記述の支援機能を持つ。
自然演繹法スタイルによる、推論規則、書き換え規則、ならびに公理の定義支援機能。推論規則は仮定を付けることを許した幾つかの前提、結論、適用条件の3部分からなる。書き換え規則は、同値な2表現からなる噴公理は、論理表現のリスト。名前をつけることができる。
人間の思考過程にあった多様な証明スタイル (たとえば、前向き、逆向きの導出の組み合わせ) を可能とする証明構築支援環境 (思考シート) を持つ。
論証向きの視覚的インタフェース。木表現のままでの規則の定義、証明の構成、論理式の木構造表示機能等を持つ。

適用論理の例

一階論理 (様々なトートロジー、停止問題の非可解性、帰納的証明)、様相命題論理(プログラムの論理)、内包論理 (モンターギュ意味論)、Martin-lofの型論理、Hoare論理 (プログラムの性質)、二階論理、一般論理、適切論理、知識の論理等。

ＦＴＰ

論証支援システム：ＥＵＯＤＨＩＬＯＳ [273K]

www-admin@icot.or.jp