Elementary Algebra Proof Exercises Using a Theorem Proving System

摘要

This paper presents the modules and features of an e-learning system which can automatically assessing the answers of elementary algebra proving problems. The system translates the answer given by a student, which is written in Chinese, into its corresponding formal proof, which is the semantic of the original sentences in the answer, and then automatically verifies the correctness of the formal proof.