| Theorem-proving is one of the important parts to learn mathematical logic, and ofwhich, the most basic one is the theorem-proving of the axiomatic system of propositionlogic. However, it is not easy for the beginners to prove a theorem merely based on axiommodes and inference rules, because the starting point of the proof can't be effectivelyfound. Instead of establishing rigorous computer-oriented mechanical methods, thepurpose of this paper is to explore practical methods for the beginners. This practicalmethods, on one hand, can make the proof achieve partial mechanization, and on the otherhand, can remain the intuitive and simple features. Thus, the beginners' readability can beenhanced, the learning efficiency can be improved, and the teaching of mathematical logiccan be optimized. Discussing the techniques and methods of the theorem-proving of theaxiomatic system of proposition logic, can also promote the development of mechanicaltheorem-proving. Therefore, it has very important theoretical and practical significances.Based on the in-depth study of previous research results and related theories, thispaper will firstly explore the universality of the axiom modes according to the fact that thetheorem-proving is always related to a certain axiomatic system. It will especially focuson exploring the functions of axiom modes in the process of proofs, and thus to obtain twopractical techniques from it——elimination and conversion. Secondly, by using these twotechniques, and combining applying synthesis method and analysis method which areoften used in mathematical proofs, we will discuss the methods and the principles ofproving simple theorems, and get the idea of making concrete analysis to concretetheorems. Finally, based on the techniques and methods of proving simple theorems andinspired by the inference of compound proposition of traditional logic, we will study onthe methods of proving complex theorems, and called it theorem-decomposition. |
PDF Full Text Request