Return to search

ProS4 - provador automático de teoremas para a lógica modal S4

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.

Identiferoai:union.ndltd.org:IBICT/oai:agregador.ibict.br.BDTD_ITA:oai:ita.br:1710
Date01 August 1993
CreatorsMarcelo Rodrigues de Souza
ContributorsCelso de Renna e Souza, Francisco Eduardo de Carvalho Viola
PublisherInstituto Tecnológico de Aeronáutica
Source SetsIBICT Brazilian ETDs
LanguagePortuguese
Detected LanguagePortuguese
Typeinfo:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis
Formatapplication/pdf
Sourcereponame:Biblioteca Digital de Teses e Dissertações do ITA, instname:Instituto Tecnológico de Aeronáutica, instacron:ITA
Rightsinfo:eu-repo/semantics/openAccess

Page generated in 0.0017 seconds