• DocumentCode
    1801249
  • Title

    Elementary algebra proof exercies using a theorem proving system

  • Author

    Bing Li ; Wei Su ; Yi Yang ; Lian Li

  • Author_Institution
    School of Mathematics and Statistics, Lanzhou University, Gansu 730000, China
  • fYear
    2013
  • fDate
    1-8 Jan. 2013
  • Firstpage
    1
  • Lastpage
    4
  • Abstract
    This paper presents the architecture of a system for automatically assessing the answers of elementary algebra proving problems. The system parses the answer given by the student, which is written in Chinese, and constructs its corresponding formal proof in a theorem proving system. Then the correctness of the formal proof, which is the semantic of the original answer, can be verified in the theorem proving system automatically.
  • Keywords
    Algebra; Educational institutions; Equations; Grammar; Mathematical model; Natural languages; Isabelle/Isar; computer aidded assessment; controlled natural language; proof problem; theorem proving system;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Conference Anthology, IEEE
  • Conference_Location
    China
  • Type

    conf

  • DOI
    10.1109/ANTHOLOGY.2013.6784786
  • Filename
    6784786