proverには担当分野があります．例えば # MESON[] `1+2=1+2`;; 0..0..solved at 2 val it : thm = |- 1 + 2 = 1 + 2 は処理できても # MESON[] `1+2=2+1`;; 0..0..1..2..6..11..19..30..41..54..81..108..149..214..279..368..489..610..763..9 96..1229..15…

現在の定理証明プログラムは ・論理式を入力すれば，自動的に証明してくれる（ものによっては証明も出力する），いわゆる，prover． 例）otter/prover9 http://www.mcs.anl.gov/research/projects/AR/otter/index.html http://www.cs.unm.edu/~mccune/mace4/…