Resumo

A construção de sistemas de demonstração automática de teoremas tornou-se possível através da formalização dos sistemas de dedução, no âmbito da teoria da dedução, e pelo surgimentos dos sistemas computacionais. No entanto a crescente complexidade dos sistemas de dedução em consideração levanta a questão da construção modular dos sistemas de dedução. Um exemplo de uma tal situação é a da construção de sistemas para demonstração da correcção de programas em linguagens do tipo procedimental.

Tendo como ponto de partida o conceito de Instituição e de Pi-instituição, assim como o tratamento categorial dos sistemas de dedução, desenvolveu-se o conceito de Sistema Lógico, como sendo uma entidade que agrega a categoria das assinaturas, a categoria dos sistemas de dedução, e um functor que para uma dada assinatura nos dá o correspondente sistema de dedução. A componente referente aos sistemas de dedução define uma categoria cujos objectos são conjuntos de sistemas de dedução, e cujos morfismo são aplicações entre conjuntos de sistemas de dedução. Demonstrou-se que a categoria dos sistemas de dedução é fechada para os co-limites. Deste modo é possível a construção, no âmbito dessa categoria, de sistemas de dedução através do cálculo de co-limites.

Foi estudada a possibilidade de aplicação destes conceitos à construção modular de um sistema de dedução para a demonstração de correcção de programas em linguagens do tipo procedimental. Tendo-se escolhido o sistema 2OBJ/OBJ3 pelas suas potencialidades de construção modular e parametrizável de programas concluiu-se no entanto que será necessário extender este sistema de forma a poder-se considerar o cálculo de co-limites na construção modular de sistemas de dedução.

Foi também brevemente analisada a possibilidade de enquadrar o estudo da fibrilação de lógicas e de sincronização de lógicas no estudo dos sistemas lógicos. Embora tal se nos afigure possível, tal aspecto carece de um estudo mais aprofundado.