命题逻辑中形式推演证明题的自动评阅系统

摘要

Automatic marking scores is the inevitable choice of large-scale computer test , but the computing symbols , operation step, and solving method of mathematics subjective problem are diversity , which always restrict the development of examination system.Mathematical logic is a branch of mathematics , and propositional logic is a part of mathematical logic .The same scheme of formal deducibility in propositional logic can have different formal proof , which means one problem has different solving meth-ods.But it has a strict procedure , so we can make use of this characteristic to develop an automatic scoring system for itself by u -sing C#.Application shows that , the system has friendly interface and it can greatly improve the efficiency of the teacher .%自动阅卷评分是大规模计算机考试的必然选择，而数学类主观题涉及运算符号、运算步骤、解题方法多样等问题，其自动评分一直制约着考试系统的发展。数理逻辑是数学的一个分支，命题逻辑是数理逻辑的一部分。命题逻辑的同一个形式可推演性模式可以有不同的形式证明，即存在一题多解的情况，但其证明有严格的程式，针对其特点用C＃开发一个适用于其自身的自动评分系统。应用表明，系统操作界面友好，可大大提高教师阅卷的工作效率。