Research On Automatic Scoring System Of Formal Deduction Proofs In Mathematical Logic

Examination plays an important role in teaching. But large number of exams will bringgreat marking workload to teachers. Traditional marking method has lots of defects, andbecause of fast and fair characteristics, the computer automatic scoring becomes a trend anda hot research topic in Computer Aided Education. Among them, the automatic scoring forsubjective questions becomes the research emphasis due to the questions’ importance andimplementation’s difficulty. But scholars’ research on automatic marking of mathematicssubjective question is little, which involves many problems such as the varieties ofcomputing symbols, operation steps and the problem solving methods.Mathematical logic is a branch of mathematics. Teachers usually based on proofs toexamine students’ mastery of the course. The distinction of mastery and knowledgeproficiency between students will cause the difference of steps and orders in the proof, andthis brings lots of trouble in marking. In the paper, formal deduction proofs of mathematicallogic are the study object. According to the characteristics of such question, an automaticscoring system is developed by using C#language in Visual Studio2010platform. Theinnovation of the paper is there is no need to match the answer of the students with thestandard answer, and the system can review the answer directly just according to the prooflogic.Mathematical logic includes propositional logic and predicate logic two parts. Thereare eleven rules in propositional and seventeen rules in predicate, the system was realizedby automatic verify the correctness of using these rules. Because the rules only involve thegrammatical structure of formulas, the system made up subfunctions for each rule.Experimental samples were stored as word documents which were taken from the students’exam answer and part of theorem proving. The system used its own interface by thebutton’s click event to complete the input of special symbol refered to the samples. Beforereviewing, the answers must be preprocessed. First, the answers were extracted by VBA(Visual Basic for Application) technology and displayed in the system interface. Second,the optimization and separation of the answers were realized. Answer separation includedstep separation, structure separation and formula separation three steps. And then formulaswere represented by binary tree after separation. The last and most important step,according to the rule of formal decuction written by the reason of every proof step, thesystem called related subfunction to verify the correctness of using formal deduction. Afterintegral testing, the system solved the trouble of hand scoring which were caused by themulti solution to one problem, and improved the teachers’marking efficiency.