一昨年に行ったように，皆さんが普段使っている定理証明系で， 同じ問題の証明をしてもらい，比較や議論を行いたいと思います．
「Problem: 無向グラフの形式化と全域木」
少し面倒ですが，是非，色々な定理証明系でやってみてもらいたいと思います．
「連結な無向グラフには全域木が存在する」を示すことを最終目標にしてみました．
全域木が存在することを示すには，以下の二つの方針があると思います．
(by Yasuhiko MINAMIDE)