Auteur principal			Co-auteurs(s)
Nom :	Dr. Gabriel Aguilera		Nom :	Dr. Jose Luis Galan
Courriel :	gabri@ctima.uma.es		Courriel :	galan@ctima.uma.es
Institution ou compagnie:	University of Malaga		Nom :	Mr. Pedro Rodriguez
Département:	Applied Mathematics		Courriel :	prodriguez@uma.es
Ville :	Malaga		Nom :	Mr. Antonio Galvez
État/Province :	Malaga		Courriel :	secretaria@academiasanmillan.com
Pays :	Spain		Nom :
Type de présentation:	Conférence :  25 minutes.		Courriel :
Conférence et numéro :	Derive & TI-CAS  ,    Numéro : D06		Horaire :   Local :	jeudi, 11h30   1350
Site Internet :
Titre de la communication :	ATPCL.mth:Automated Theorem Provers for Propositional Classical Logic withDERIVE
Résumé de la communication :
In this paper the file ATPCL.mth is presented. This file has been developed for using DERIVE as an automated theorem prover for Propositional Classical Logic by means of different algorithms such as “Quine”, “Semantic Tableaux” and “Short Normal Form + Resolution”. The use of this utility file is specially useful for teachers and students in subjects on Computational Logic in Computer Science degree. In particular, the file can be used as a didactical tool for helping in the teaching and learning of automated logic deduction process. In order to develop these algorithms, another utility file has been created to deal with tree structure using the new features of programming in DERIVE. In this paper this utility file (tree.mth) will be also described. The use of these utility files will be presented by means of some examples about validity, satisfiability and deduction using both utility files. Finally, conclusions and future work will be shown.