Title :
Automatic Assessment of Proving Problems in Middle School Algebra
Author :
Li, Bing ; Liu, Li ; Li, Lian
Author_Institution :
Sch. of Math. & Stat., Lanzhou Univ., Lanzhou, China
Abstract :
Automatic assessment of proving problems is very important is mathematic e-learning systems. It accepts the answer of a proving problem, which can be written in a controlled natural language, and then translates it into a formal proof, e.g. in Isabelle/Isar. The correctness of the original answer is equivalent to that of the formal one obtained from the translation, which can be verified in a theorem prover automatically. In this paper, we describe a method which can be used to verify such formal proofs in theorem proving systems.
Keywords :
algebra; computer aided instruction; mathematics computing; natural language processing; theorem proving; automatic proving problems assessment; controlled natural language; formal proof; mathematic e-learning systems; middle school algebra; theorem proving systems; Algebra; Artificial intelligence; Cognition; Educational institutions; Engines; Equations; Mathematical model; Isabelle/Isar; automatic assessment; controlled automatic theorem proving; elemtentary algebra;
Conference_Titel :
Intelligent Human-Machine Systems and Cybernetics (IHMSC), 2011 International Conference on
Conference_Location :
Zhejiang
Print_ISBN :
978-1-4577-0676-9
DOI :
10.1109/IHMSC.2011.121
