Teaching Semantic Tableaux Method for Propositional Classical Logic with a CAS

摘要

Automated theorem proving (ATP) for Propositional Classical Logic is an algorithm to check the validity of a formula. It is a very well-known problem which is decidable but co-NP-complete. There are many algorithms for this problem. In this paper, an educationally oriented implementation of Semantic Tableaux method is described. The program has been designed to be used as a pedagogical tool to help in the teaching and learning process of the subject Propositional Classical Logic. Therefore, the main goal of the implementation is not to be very efficient but to get a useful tool for education. For this reason, the implementation of the Semantic Tableaux method provides an optional graphical approach which shows, step by step, the trace of the algorithm when applied to a specific problem. The algorithm has been implemented using a CAS (Computer Algebra System), specifically DERIVE, as part of the students training in Mathematics for Engineering. The result is a utility file containing a didactical implementation of the Semantic Tableaux algorithm which can be used not only at lectures but as a self-learning tool by students. With this utility file, students can check the results obtained by hand and, in case they get a wrong result, students can find the step where the mistake occurred. Furthermore, if the student does not know how to solve an exercise, the utility file can show how to overcome this situation step by step. Since Derive does not have the Semantic Tableauxs algorithm implemented, this utility file increases the capabilities of this CAS. Therefore, Derive can act as an automated theorem prover for Propositional Classical Logic from a PeCAS (Pedagogical CAS) point of view. The description of how to use this utility file will be shown throughout different examples related to validity, satisfability and deduction, which are the main kind of problems that an ATP can solve. Finally, since the Semantic Tableaux algorithm uses a tree structure, another utility file has been developed to deal with trees. In this paper, this utility file is also described.