Main presenter
Co-presenter(s)
Name :
Dr. Gabriel Aguilera
Name:
Dr. Jose Luis Galan
E-mail:
gabri@ctima.uma.es
E-mail:
galan@ctima.uma.es
Institution or
Company:
University of Malaga
Name:
Mr. Pedro Rodriguez
Department:
Applied Mathematics
E-mail:
prodriguez@uma.es
City:
Malaga
Name:
Mr. Antonio Galvez
State/Province:
Malaga
E-mail:
secretaria@academiasanmillan.com
Country:
Spain
Name:
Type of
presentation:
Lecture : 25 minutes.
E-mail:
Conference
strand and number:
Derive & TI-CAS ,
Number:
D06
Schedule:
Room:
Thursday, 11h30
1350
Related website:
Title of
presentation:
ATPCL.mth:Automated Theorem Provers for Propositional Classical Logic withDERIVE
Abstract:
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.