推論（正確にはリーズニング）に関して次の4分類をする。 正しい 間違っている 受け入れやすい 問題なし 誤用（アブダクション） 受け入れにくい 難解 問題なし 推論を順推論（通常の推論）と逆推論（バックワードリーズニングの原子ステップ）に分ける。問…

1. 連言 ∧ A B A∧B ------ ------ A∧B A - A∧B -A -------(分割統治) --------(過剰責務) -A -B - A∧(B) 2. 選言 ∨ A A∨B [A |- C, B |- C] ------- ------------------------- A∨(B) C - A∨B -C -------(投機) ----------------------------- -A - (A)∨(B) …

Isarのbyはボディがない証明（proof eqd）の略記。byの直後は証明メソッド。 Mizarは推論規則の適用とスキーマの適用をby, fromで区別するが、Isarは高階論理なのでbyだけ。 Isarの前置fromはMizarのfromとは別。Mizarのby相当らしいが要チェック。 Isarの前…