DocumentCode
1598652
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
Volume
2
fYear
2011
Firstpage
205
Lastpage
208
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Intelligent Human-Machine Systems and Cybernetics (IHMSC), 2011 International Conference on
Conference_Location
Zhejiang
Print_ISBN
978-1-4577-0676-9
Type
conf
DOI
10.1109/IHMSC.2011.121
Filename
6038251
Link To Document