Título: Complexidade Descritiva da Lógica de Ponto Fixo Relacional Inflacionário.

Data: 10/06/2016 Horário: 11h Local: Sala de Seminários - Bloco 952

Resumo:

Complexidade Descritiva é um ramo da Teoria dos Modelos Finitos que está interessada em caracterizar classes de complexidade computacionais em termos dos recursos lógicos necessários para expressar todos os problemas que estão contidos na classe. O resultado mais celebrado da área é o Teorema de Fagin [Fagin74] que prova que a classe NP é capturada pelo fragmento existencial de segunda ordem. Por outro lado, a lógica de primeira ordem não é expressiva o suficiente para definir problemas simples como o problema da conectividade de grafos. A introdução de operadores de ponto fixo é uma técnica padrão para acrescentar poder expressivo à lógica de maneira controlada. De fato, em [Immerman82] e [Vardi1982] é provado que a lógica de primeira ordem com o operador de menor ponto fixo, denotada por LFP, é capaz de capturar a classe P sobre estruturas finitas e ordenadas. Nosso trabalho é comparável ao trabalho descrito por Abiteboul, Varde, e Vianu em [AVV97], o qual introduz a noção do ponto fixo não-determinístico e prova que a lógica de primeira ordem com tal operador captura a classe NP sobre estruturas ordenadas. Neste trabalho, seguiremos uma abordagem diferente e definiremos a noção de ponto fixo sobre uma relação arbitrária. Nós generalizamos as lógicas clássicas de ponto fixo usando relações no lugar de operadores. A ideia básica é que usamos laços em uma relação no lugar de pontos fixos de uma função, isto é, X é ponto fixo de uma relação R no caso do par (X,X) pertencer a relação R. Nós introduzimos a noção de ponto fixo inicial de uma relação inflacionária R e o operador rifp associado. Denotamos por RIFP a lógica de primeira ordem com o operador de ponto fixo relacional inflacionário e mostramos que essa lógica captura a hierarquia polinomial usando uma tradução para a lógica de segunda ordem. Também consideramos o fragmento RIFP1 com a restrição do operador rifp poder ser aplicado no máximo uma vez. Mostramos que RIFP1 captura a classe NP e comparamos nossa lógica com a lógica de ponto fixo não-determinístico proposta por Abiteboul, Vianu e Vardi em [AVV97].

Banca:

• Prof.ª Dr.ª Ana Teresa de Castro Martins (MDCC/UFC- Orientadora)
• Dr. Francicleber Martins Ferreira (UFC - Coorientador)
  
• Prof. Dr. Edward Hermann Haeusler (PUC-Rio)
• Prof. Dr. Ruy José Guerra Barretto de Queiroz (UFPE)
• Prof. Dr. Pedro Porfírio Muniz Farias (UNIFOR)
• Prof. Dr. João Fernando Lima Alcântara (MDCC/UFC)