矛盾を含んだ命題集合からは、有限回の手順によって必ず矛盾が発見される。(1965年Robinson,J.A.によって証明)
上記の証明によって、命題Aが正しいと仮定し、それを否定することによって命題を矛盾させ￢Aとし、￢Aの全てを積に置き換え、その積のうち１ヶ所でも矛盾していたら、全体が矛盾し、結果、命題Aは正しいという事ができる。
通常の証明方法と比べ手順が多くなるが、これによって、コンピュータによる完全証明チェックシステムが可能になった。
最初にsuch that,hold,impliesの意味の違いについて私は戸惑った。
何故ならば、様々なMizarの説明書によって書き方が統一されていなかったからである。
その後、トートロジーで示すと全て等価な形式で示すことが可能であることが分かった。
しかし、せめて書き方の作法として、
と言う点に注意をした方が可読性が高まると思われる。
また、コンピュータの処理手順に従って記述した方が、エラーも少なく、かつ、コンピュータの内部処理としては効率的である。
しかし、今後の論理証明を行う上で人間が考察しやすいように何かしら改善の余地が必要であると考えられる。
数学の証明するには論理記号を使い、
 空間条件(論理集合(論理式)):性質
と言った形式で表現しなければならない。
 空間条件定義
  ∀,∃。自然数、整数、実数、複素数などによる変数、定数、範囲を指定する。それの終了は"such that","st"で区切る。
 論理集合の演算(範囲、領域)
  否定￢
  論理集合2⊂論理集合2
   ⊂ holds 、∪ or 、∩ &
 論理式(点空間)
  ⇒ implies、⇔ iff(if not only if) 、/\ ∧、 \/ ∨
 変換演算
  加減乗除、微分、積分、外積、内積、など