id: 06597689
dt: j
an: 2016d.00962
au: Aguilera-Venegas, Gabriel; Galán-García, José Luis; Galán-García,
María Ángeles; Rodríguez-Cielos, Pedro
ti: Teaching semantic tableaux method for propositional classical logic with a
CAS.
so: Int. J. Technol. Math. Educ. 22, No. 2, 85-91 (2015).
py: 2015
pu: Research Information Ltd, Burnham, Bucks
la: EN
cc: U70 E30 N80
ut: classical propositional logic; semantic tableaux method; computer algebra
system
ci:
li: http://www.researchinformation.co.uk/time/contents/timecont.php
ab: Summary: 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.
rv: