Sistemas de dedução para lógicas modais proposicionais

Este trabalho apresenta uma descrição sucinta dos fundamentos de lógicas modais (propriedades como derivabilidade, relação de conseqüência, completude e corretude), bem como de seus principais sistemas de dedução. As lógicas modais oferecem um aumento acentuado da capacidade de expressar estruturas de espaço, estado ou tempo, comparativamente à capacidade apresentada pela lógica clássica. O interesse nessas lógicas é justificado, pois elas são utilizadas para especificar e raciocinar sobre propriedades comportamentais de modelos e aplicações em Ciência da Computação. Entre os sistemas dedutivos descritos, estão incluídos o sistema axiomático, o sistema de dedução natural, o sistema de tableaux, o sistema de resolução e os sistemas rotulados. Cada um dos sistemas dedutivos é descrito em um capítulo individual. Ao final do texto, é apresentada a comparação estabelecida entre os sistemas de prova estudados. Por fim, são esboçadas as conclusões e trabalhos futuros suscitados pela pesquisa.