>>115
一方で、自動証明はダメといいつつ、
もう一方で、行数を少なくしろといってること。

行数を少なくすれば、行間が広くなる。
そこは、単純に推論規則に当てはまってるかどうか
だけではチェックできない。行間を埋められるような
推論規則の組み合わせが存在するかどうかを確かめる
必要がある。それはまごうことなき「自動証明」だ