Abstract: 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 methods. But it has a strict procedure, so we can make use of this characteristic to develop an automatic scoring system for itself by using C#. Application shows that, the system has friendly interface and it can greatly improve the efficiency of the teacher.

Key words: formal deduction, propositional logic, formal proof, automatic marking, C#