Pedro Quaresma de Almeida, Construção Modular de Sistemas de Dedução, Tese de Doutoramento, Departamento de Informática da Universidade do Minho, 1998.

Summary

The construction of automatic proof systems has been made possible by the formalization of proof systems in the scope of proof theory, and by the development of computers. The increasing complexity of the proof systems under development raises the need of the modular construction of proof systems. As an example we may consider the construction of proof systems for the automatic proof of program correctness.

Having the definition of Institution, Pi-Institution, and the categorical viewpoint of proof systems as a starting point, we have developed the concept of Logic System. A Logic System consists of: a category of signatures; a category of sets of proof systems; and a functor connecting signatures with the corresponding set of proof systems. We have proved that the category of proof systems is cocomplete, therefore it is possible to use colimites to built proof systems.

We have tried to apply these concepts in the modular construction of a proof system for the proof of program correctness. We have chosen the 2OBJ/OBJ3 system for its modular and parametrized program construction capabilities. We have concluded however that it is necessary to extend this system in order to have the capabilities of colimite constructors.

The study of fibring of logics, and the synchronization of logics in the Logic Systems setting was briefly analyzed. Although we consider this a feasible approach, it will require further study.