自動定理証明 - ATPとCASのこと現在の定理証明プログラムは ・論理式を入力すれば，自動的に証明してくれる（ものによっては証明も出力する），いわゆる，prover． 例）otter/prover9 http://www.mcs.anl.gov/research/projects/AR/otter/index.html http://www.cs.unm.edu/~mccune/mace4/ SPASS http://www.spass-prover.org/ そして，Theorema http://www.risc.jku.at/research/theorema/description/ ・証明に用いる定理や規則を対話的に入力する，いわゆる，proof assistant． 例）LCF http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/reasonng
