Towards an algebrization of a linear temporal logic

Resumo

O presente trabalho trata da L´ogica Proposicional da Vizinhança (LPV), um caso de l´ogica temporal linear e uma extens˜ao da L´ogica Proposicional Cl´assica dada pelo acr´escimo de operadores modais que tratam de certos aspectos temporais. Nesse contexto, a validade de uma proposição est´a estritamente relacionada a algum intervalo de tempo. Destacamos alguns aspectos formais dessa l´ogica e a sua formalização em sistemas dedutivos (ou de provas), que naturalmente retratam os aspectos formais do tempo. Pretendemos investigar modelos alg´ebricos para a L´ogica Proposicional da Vizinhança. Todavia, neste trabalho, nos dedicamos apenas `a apresentac¸˜ao do resultado de Correção, uma das etapas necess´arias para a obtenção de um modelo adequado (correto e completo), entre o sistema axiom´atico da LPV e o pretendido modelo alg´ebrico.