14/09/07 13:39:22.65
文書がながくなってわかりにくくなったので箇条書きにすると以下です。
* すれ主さんの探してくれたソフトのソースは多分 GAPでわたしが昨日サルマネできるようになったのと同じかそれに似た具体的な方程式が決まってる場合の処理ソフトだと思います。
* GAPの方が群論ソフトとしては特化してる分だけ記述量少なくて同じ処理が可能だと思います。
* 昨日探した証明ソースは証明そのものを補助あるいは、自動で証明(かんたんなもの)ができるソフトのソースで、具体性がなくても処理可能なソフト。
(数値と数式で言うと、数式処理ソフトは式の評価が可能ですよね。
同じように定理と証明を補助することができるソフトや証明そのものを自動で行なえるソフトがあって
そっち系のソフトを探してました。
)
* the Odd Order Theoremは有名なFeit?Thompson theoremで 、それをその証明補助ソフトを使って証明チェックしたソースらしきものがあった。
欲しいものじゃなかったのでURLは忘れてしまった。上のキーワードでネット検索すればみつかると思います。)
* 欲しいのは、一般的な皆が本で苦しんで理解できた証明を、証明補助ソフトあるいは自動ソフトで証明あるいは確認できるソース。
* 演算を追加して可解になるかどうかをその証明補助ソフトで確認できたら理想。