NotesFAQContact Us
Search Tips
Peer reviewed Peer reviewed
Direct linkDirect link
ERIC Number: EJ1079164
Record Type: Journal
Publication Date: 2015
Pages: 7
Abstractor: As Provided
ISSN: ISSN-1744-2710
Teaching Semantic Tableaux Method for Propositional Classical Logic with a CAS
Aguilera-Venegas, Gabriel; Galán-García, José Luis; Galán-García, María Ángeles; Rodríguez-Cielos, Pedro
International Journal for Technology in Mathematics Education, v22 n2 p85-91 2015
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, satisfiability 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.
Research Information Ltd. Grenville Court, Britwell Road, Burnham, Buckinghamshire, SL1 8DF, UK. Tel: +44-1628-600499; Fax: +44-1628-600488; e-mail:; Web site:
Publication Type: Journal Articles; Guides - Classroom - Teacher; Reports - Descriptive
Education Level: Higher Education; Postsecondary Education
Audience: Teachers
Language: English
Sponsor: N/A
Authoring Institution: N/A
Grant or Contract Numbers: N/A