>>970
キーワードありがとうございます
先の私の発言 >>960 は coq を念頭に置いたものでしたが、証明支援と自動定理証明とは別の世界だったようですね…
coq では人間様が証明の方針を入力しなければならない（と思っています）のですが、それとは別に総当りで証明を組み立てるシステムがある、という理解でいいですか？