Computational Logic Group
The research activities of our group in the area of automated theorem proving begun at the end of the eighties, mainly focused on the application of algebraic methods (Gröbner basis) to deduction in multivalued logics.
In the second half of the nineties, we started to apply algebraic methods to the verification of knowledge-based systems. In 1997, we begun our project to apply formal methods to the verification of reasoning systems. Using ACL2 we have developed a number of basic computational theories for automated deduction.
Currently, the group is formed by seven members. Our main research interests are:
- the study of techniques allowing to increase the efficiency of the algorithms of the computational theories previously developed,
- the application of the techniques developed to the verification, with the PVS verification system, of other intelligent systems (like formal concept analysis), and
- the study of the validation of knowledge bases in complex ontologies and its applications to the Semantic Web.