自動定理証明を応用した数学コースウェアの開発 Development of a Mathematical Courseware using Automated Theorem Proving

We illustrated idea of mechanical theorem proving and outline of the CAI courseware under planing, which uses method of mechanical theorem proving. Mechanical theorem proving is applicable to theorem proving, answer questioning and problem solving system. By using the method it will be possible to construct the CAI courseware on mathematics which helps student to learn theorem proving problem at secondary school lebel. The CAI courseware gives student theorem proving problems, accepts the answer, diagnoses it whether there are logical contradictions and leaps and gives student knowledge of result for the problems.