ProS4 - provador automático de teoremas para a lógica modal S4
AUTOR(ES)
Marcelo Rodrigues de Souza
FONTE
IBICT - Instituto Brasileiro de Informação em Ciência e Tecnologia
DATA DE PUBLICAÇÃO
01/08/1993
RESUMO
A Logica Modal tem sido utilizada em Ciencia da Computacao no tratamento de crencas, conhecimento, processamento de linguagem natural, analise de sistemas distribuidos, verificacao de programas concorrentes e paralelos, e raciocinio temporal. Estas aplicacoes requerem o desenvolvimento de provadores automaticos de teoremas para os sistemas modais utilizados nas suas formalizacoes. Este trabalho nas suas formalizacoes. Este trabalho apresenta a implementacao de um provador de teoremas para o sistema modal S4, denominado ProS4. Utilizam-se os tableaux semanticos de Fitting, sendo introduzidas novas heuristicas e estruturas de dados que fazemo provador ser eficiente, sem perder a decidibilidade. Na verificacao da validade ou nao de uma formula modal, o provador apresenta a demonstracao ou o modelo falsificador da formula em questao. O ProS4 pode ser extendido a Logica Temporal Linear de Programas, atraves da adicao do operador proximo (next) e linearizacao na geracao de novos mundos.
ASSUNTO(S)
lógica modal representação do conhecimento linguagem natural (computadores) processamento de dados lógica matemática computação matemática
