Paper Titles

Research of Filtering Method for ESPI Fringe Patterns
p.3195

A Noval Distributed Architecture for Expression Recognition
p.3199

An Approach to Obtain Software Security Vulnerabilities Based on Vertical Search
p.3203

Research on Decomposition of Toluene Using Adsorption Combined with Non-Thermal Plasma
p.3207

Semantic Interpretation of the Answers of Elementary Algebra Proving Problems
p.3212

On-Line Identification of Process Model Based on Swarm Intelligence Technology
p.3216

Life Cycle Cost Analysis of the Fuel Cell Bus Based on Chinese Bus Cycle
p.3220

A Methodological Approach to Bus-Equipped Automotive ECU Test System Using Modeling and Parsing of Script Language
p.3224

A Novel Optimization and Control Method for Signalized Traffic Network
p.3229

HomeAdvanced Materials ResearchAdvanced Materials Research Vols. 403-408Semantic Interpretation of the Answers of...

Semantic Interpretation of the Answers of Elementary Algebra Proving Problems

Article Preview

Abstract:

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.

You might also be interested in these eBooks

MEMS, NANO and Smart Systems

Info:

Periodical:

Advanced Materials Research (Volumes 403-408)

Pages:

3212-3215

DOI:

https://doi.org/10.4028/www.scientific.net/AMR.403-408.3212

Citation:

Cite this paper

Online since:

November 2011

Authors:

Bing Li, Yi Yang, Lian Li

Keywords:

Computer Aided Assessment, Natural Language Understanding, Theorem Proving

Export:

RIS, BibTeX

Price:

Permissions CCC:

Request Permissions

Permissions PLS:

Request Permissions

Сopyright:

© 2012 Trans Tech Publications Ltd. All Rights Reserved

Share:

Citation:

[1] Tobias Nipkow, Lawrence C. Paulson, and M. Wenzel, Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, 2002. LNCS Tutorial 2283.

[2] A. Ranta, "Grammatical Framework: A Type-Theoretical Grammar Formalism," Journal of Functional Programming, 14(2), 2004, pp.145-189.

[3] Grammatical Framework: http://www.grammaticalframework.org.

[4] R.P. Nederpelt, J.H. Geuvers, and R.C. de Vrijer (editors), "Selected Papers on Automath," volume 133 of Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1994.

DOI: 10.1016/s0049-237x(08)70195-2

[5] Rob Nederpelt, "Weak Type Theory: A formal language for mathematics," Computing Science Report 02-05, Eindhoven University of Technology, Department of Math. and Comp. Sc., 2002.

[6] F. Kamareddine, M. Maarek, and J.B. Wells, "MathLang: An experience driven language of mathematics," Electronic Notes in Theoretical Computer Science, 93C, 2004, pp.138-160.

DOI: 10.1016/j.entcs.2003.12.032

[7] F. Kamareddine, J. B.Wells, "Computerizing Mathematical Text with MathLang," Electron. Notes Theor. Comput. Sci. 205, 2008, pp.5-30.

DOI: 10.1016/j.entcs.2008.03.063

[8] P. Rudnicki, "An Overview of the MIZAR Project," Proc. 1992 Workshop on Types and Proofs for Programs, 1992, pp.311-332.

[9] M. Wenzel, F. Wiedijk, "A Comparison of Mizar and Isar," Journal of Automated Reasoning, vol. 29, 2002, pp.389-411.

[10] Zinn C, "Understanding Informal Mathematical Discourse," PhD thesis, Friedrich-Alexander-University Erlangen Nurnberg, 2004.

[11] H. Kamp and U. Reyle, From Discourse to Logic, Kluwer Academic Publishers, 1993.

[12] D. Kuhlwein, M. Cramer, P. Koepke, and B. Schröder, The Naproche System. In Intelligent Computer Mathematics, Springer LNCS, ISBN: 978-3-642-02613-3, 2009.

[13] M. Humayoun and C. Raalli, "MathNat - Mathematical Text in a Controlled Natural Language," 11th International Conference on Intelligent Text Processing and Computational Linguistics (CICLing 2010), Iai, Romania, 2010, pp.293-310.

DOI: 10.1007/978-3-642-12116-6

[14] C. J. Sangwin, "Assessing Elementary Algebra with STACK," International Journal of Mathematical Education in Science and Technology, 38(8), 2008, p.987–1002.

DOI: 10.1080/00207390601002906

[15] W. Billingsley and P. Robinson, "Student Proof Exercises Using MathsTiles and Isabelle/HOL in an Intelligent Book," Journal of Automated Reasoning, vol. 39, 2007, pp.181-218.

DOI: 10.1007/s10817-007-9072-3