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.
| Identifer | oai:union.ndltd.org:IBICT/oai:agregador.ibict.br.BDTD_ITA:oai:ita.br:1710 |
| Date | 01 August 1993 |
| Creators | Marcelo Rodrigues de Souza |
| Contributors | Celso de Renna e Souza, Francisco Eduardo de Carvalho Viola |
| Publisher | Instituto Tecnológico de Aeronáutica |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Format | application/pdf |
| Source | reponame:Biblioteca Digital de Teses e Dissertações do ITA, instname:Instituto Tecnológico de Aeronáutica, instacron:ITA |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0019 seconds