Teaching Semantic Tableaux Method for Propositional Classical Logic with a CAS
Gabriel Aguilera‐Venegas, José Luis Galán–García, María Ángeles Galán–García, Pedro Rodríguez–Cielos · International Journal for Technology in Mathematics Education · 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.