Semantic Interpretation of the Answers of Elementary Algebra Proving Problems
Bing Li, Yi Yang, Lian Li · Advanced materials research · 2011
This paper describes the semantic interpretation of a restricted language in a system which automatically assesses the answer of a proving problem of elementary algebra in Chinese. The system translates a student’s proof into a formal one which can be verified in Isabelle/Isar automatically. The correctness of the original proof is equivalent to the formal one obtained from the translation.