命題論理の演繹エディタ

命題論理の演繹エディタです。関連付けられている仮定を表示しながら正しく演繹が行われているかをチェックすることができます。
ツリー式ではなく、番号付きの行を参照する方式です。
公理系は次のものを採用しています。

• 結合子・論理演算子は⊃（「ならば」、含意）、￢（「でない」、否定）、∧（「かつ」、連言）、∨（「または」、選言）です。

• 推論規則は次の通りです。

  • ASP　…　任意の式を仮定できる。その行自身が仮定となる。
  • ⊃+　…　行ａ“Ｐ”（仮定の行に限る）を仮定として行ｂ“Ｑ”を導くことができたとき“Ｐ⊃Ｑ”を導くことができる。その際、行ｂの仮定（行ａ以外のもの）を引き継ぐ。
  • ⊃-　…　行ａ“Ｐ”と行b“Ｐ⊃Ｑ”から“Ｑ”を導くことができる。その際、行ａと行ｂの仮定をすべて引き継ぐ。
  • ￢+　…　行ａ“Ｐ⊃(Ｑ∧￢Ｑ)”から“￢Ｐ”を導くことができる。その際、行ａの仮定をすべて引き継ぐ。
  • ￢-　…　行ａ“￢￢Ｐ”から“Ｐ”を導くことができる。その際、行ａの仮定をすべて引き継ぐ。
  • ∧+　…　行ａ“Ｐ”と行ｂ“Ｑ”から“Ｐ∧Ｑ”を導くことができる。その際、行ａと行ｂの仮定をすべて引き継ぐ。
  • ∧-1　…　行ａ“Ｐ∧Ｑ”から“Ｐ”を導くことができる。その際、行ａの仮定をすべて引き継ぐ。
  • ∧-2　…　行ａ“Ｐ∧Ｑ”から“Ｑ”を導くことができる。その際、行ａの仮定をすべて引き継ぐ。
  • ∨+1　…　行ａ“Ｐ”から“Ｐ∨Ｑ”を導くことができる。その際、行ａの仮定をすべて引き継ぐ。
  • ∨+2　…　行ａ“Ｑ”から“Ｐ∨Ｑ”を導くことができる。その際、行ａの仮定をすべて引き継ぐ。
  • ∨-　…　行ａ“Ｐ∨Ｑ”、行ｂ“Ｐ⊃Ｒ”、行ｃ“Ｑ⊃Ｒ”から“Ｒ”を導くことができる。その際、行ａ、行ｂ、行ｃの仮定をすべて引き継ぐ。

• 仮定なく、“Ｐ”を導くことができたら、Ｐの演繹は終了です。

命題論理の演繹エディタ

命題論理の演繹を入力していくエディタです。関連付けられている仮定を確認しながら演繹が正しく行われているかをチェックできます。