Mizar/証明思考法
< Mizar
コンピュータによる、定理の自動証明法（導出原理の完全性）
[編集]矛盾を含んだ命題集合からは、有限回の手順によって必ず矛盾が発見される。(1965年Robinson,J.A.によって証明)
上記の証明によって、命題Aが正しいと仮定し、それを否定することによって命題を矛盾させ￢Aとし、￢Aの全てを積に置き換え、その積のうち１ヶ所でも矛盾していたら、全体が矛盾し、結果、命題Aは正しいという事ができる。 通常の証明方法と比べ手順が多くなるが、これによって、コンピュータによる完全証明チェックシステムが可能になった。
| 順番 | 操作 | 式 | 変換前 | 変換後 | 真 | |
| ① | 存在記号と全称記号を削除 | 式に含まれる存在記号を消すと、全称記号が無条件で消せる | ∧(∨(∀x∃y st (g(x,y) hold f(x,y)))) | 1 | ||
| a | 存在作用素の除法 | 式に含まれる存在記号を消す為に、関数(Skolem関数:限定作用素)へ変換する | ∧(∨(∀x st (g(x,y(x)) hold f(x,y(x))))) | ∃y | y(x) | 1 |
| b | 変数名の変更（標準化） | 各限定作用素Fは独立なので、変数名称を重ならないように変更する。 | 1 | |||
| c | 全称記号を移動 | 全称記号を全て前方へ移動する。 | ∀x st (∧(∨g(x,y(x)) hold f(x,y(x)))) | ∀x st F | 1 | |
| d | 全称記号を削除 | 全称記号を変換後、削除する(∀x→F＝∃x∨F＝F)。思想として異なるが、処理系ではsuch that, hold ,impliesは全て同じ。 | ∧(∨(g(x,y(x)) hold f(x,y(x)))) | ∃x∨ | 削除 | 1 |
| ② | 合意文字(⇒)の置換 | 全ての公理を節形式(￢,∧,∨)に変換する。(トートロジーとしてはhold(⊆)とimplies(⇒)は同じ) | ∧(∨(￢g(x,y(x)) ∨ f(x,y(x)))) | A⇒B | ￢A∨B | 1 |
| ③ | 否定変換 | 全否定をすることによって、正しい＝真(1)、偽(0)、を矛盾＝真(0)、偽(1)へと反転させる。 | 0 | |||
| a | 全否定 | 全ての式を否定する | ￢(∧(∨(￢g(x,y(x)) ∨ f(x,y(x))))) | F | ￢F | 0 |
| b | 否定記号(￢)の範囲縮小 | ￢をただ一つの述語記号(ＡやＢなど)のみに適応させる | ∨(∧(g(x,y(x)) ∧ ￢f(x,y(x)))) | ￢￢A | A | 0 |
| ④ | 掛け算への変換 | 全て、節(∨でリテラル{Ａや￢Ａなど}をつないだもの)の掛け算に変換する。どれか１つの節が0になれば全体が0として示せる。 | 0 | |||
| a | 積標準形への変換 | Ａ∧(Ｂ∨Ｃ)→(Ａ∨Ｂ)∧(Ａ∨Ｃ)と節Ａ:(Ａ∨Ｂ)と節Ｂ:(Ａ∨Ｃ)などに全て変換し置き換える | ∧(G∨F) | 0 | ||
| ⑤ | 同じ形の節を1つにする | ２つの節Ａと節Ｂが同じ形にすること(単一化:ユニフィケーション)が可能ならば、削除する。 | ∧Z | (A∨B)∧(A∨B) | (A∨B) | 0 |
| ⑥ | 節を一つづつ0になるか確認 | 一つの節でも矛盾すれば真(0)となり証明終了、しない場合はその節を１と置いて消し⑤に戻り、次の節を処理する。 | どれか一つでもZが0ならば、∧Zは0になる。 | 0 |
最初にsuch that,hold,impliesの意味の違いについて私は戸惑った。 何故ならば、様々なMizarの説明書によって書き方が統一されていなかったからである。 その後、トートロジーで示すと全て等価な形式で示すことが可能であることが分かった。 しかし、せめて書き方の作法として、
∀x such that f(x) ∃x∨f(x) f(x) 定義変数xと式f(x)を分けるときに使うもの。 A hold B A⊆B ￢A∪B ある領域Aとある領域Bの包含関係を示すときに使うもの。 a implies b a⇒b ￢a∨b ある点aから、ある点bへの写像を示すときに使うもの。
と言う点に注意をした方が可読性が高まると思われる。
また、コンピュータの処理手順に従って記述した方が、エラーも少なく、かつ、コンピュータの内部処理としては効率的である。
しかし、今後の論理証明を行う上で人間が考察しやすいように何かしら改善の余地が必要であると考えられる。
論理の内包順
[編集]数学の証明するには論理記号を使い、
空間条件(論理集合(論理式)):性質
と言った形式で表現しなければならない。
空間条件定義 ∀,∃。自然数、整数、実数、複素数などによる変数、定数、範囲を指定する。それの終了は"such that","st"で区切る。
論理集合の演算(範囲、領域) 否定￢ 論理集合2⊂論理集合2 ⊂ holds 、∪ or 、∩ &
論理式(点空間) ⇒ implies、⇔ iff(if not only if) 、/\ ∧、 \/ ∨
変換演算 加減乗除、微分、積分、外積、内積、など