自動証明における自然な証明生成への一つの近接
スポンサーリンク
概要
- 論文の詳細を見る
1階述語論理における自動証明について,与えられた論理式A_0に対する妥当性検証手続きが肯定的に終了するとき,そのとき得られるある種の情報をguideとするならば,論理式A_0のLK証明図を生成することが可能である.ここではさらにこのようにして得られたLK証明図を人の証明に近づける変換アルゴリズムを連結し,自然な証明の生成を一貫した自動証明手続きにより行うことへの一つの近接を試みる.すなわち以下では,自動証明で得られたLK証明図の中に潜在する`場合分け証明に関する情報'等を顕現化することにより,排中律型公理の下で三段論法を含む自然な証明へ変換するアルゴリズムの一つが提示される.
- 一般社団法人情報処理学会の論文
- 1994-02-15
著者
関連論文
- 知識命題の標準形を用いる妥当性検証(アルゴリズムと計算量理論)
- 自動証明における自然な証明生成への一つの近接
- 自動証明における自然な証明生成の1アルゴリズム(理論計算機科学とその周辺)
- 自動証明における自然な三段論法の導入について : (LJ + 排中律)証明への変換アルゴリズムによる(数学基礎論とその応用)
- N-set partitionsを用いる妥当性検証プログラムの実際について
- 付随式を用いる1階述語論理の妥当性検証手続
- 付随式を用いる1階述語論理の証明図作成方法 (形式言語理論とオートマトン理論)
- 妥当性検証時の情報を利用する論理式の証明図作成方法
- 妥当な論理式(1階述語論理)の証明図作成の1つの方法 (計算機科学の数学的基礎)
- ベル数B(N)の1つの算式 (計算機科学の数学的基礎)
- 自動証明における自然な三段論法の導入--自然な証明生成への1つの近接
- エルブランの定理の構成的証明
- guide情報を利用する証明のプログラミング (ゲ-デル)
- エルブランの定理にもとずく1階述語論理の論理式の妥当性検証プログラムの1つについて