Lógica, Provas e Algoritmos

[ Próxima Página | Página Anterior | Página Principal ]

Uma Breve Descrição das Áreas Identificadas como Fronteiriças

Computer-Aided Verification
Computer-Aided Verification estuda algoritmos e estruturas para suportar as atividades de verificação de propriedades de programas. Utiliza técnicas provenientes de teoria dos grafos, combinatória, teoria dos autômatos, funções e álgebras booleanas, lógica matemática, teoria de Ramsey e programação linear. Observa-se que o interesse da comunidade científica sobre o tópico tem crescido significativamente, principalmente desde a realização do DIMACS CAV Workshop em 1990, não apenas no ambiente acadêmico, mas também nas grandes companhias como Intel, DEC, Sun e AT&T. Tudo isto propicia uma oportunidade rara e recompensadora de se ver teoria colocada diretamente na prática.

Finite-Model Theory
Teoria dos Modelos é o estudo de estruturas matemáticas que satisfazem conjuntos de axiomas. Trabalhos recentes sobre modelos FINITOS de um conjunto de axiomas tem produzido relações bastante elegantes entre Teoria dos Modelos e Teoria da Computação, incluindo a caracterização de classes de complexidade de algoritmos baseada em modelos. Além do mais, quando uma estrutura matemática vem equipada com medidas de probabilidade pode-se desenvolver meta-teoremas bastante poderosos chamados `leis 0-1', que fornecem condições sob as quais probabilidades devem se aproximar de 0 ou 1 quando o tamanho da estrutura tende ao infinito.

Proof Complexity
Duas noções intimamente relacionadas de complexidade de prova têm motivado a maioria dos trabalhos recentes na interface entre Ciência da Computação e Lógica Matemática. Uma delas gira em torno da questão do comprimento de uma prova, e a outra trata da complexidade de passos de inferência dentro de uma prova. Sabe-se muito bem que NP=co-NP se e somente se todas as tautologias proposicionais têm provas curtas. Mas as conecções entre o comprimento de provas e a teoria da complexidade vai muito mais além. Limites inferiores em circuitos são intimamente ligados aos limites de comprimento de prova em sistemas formais restritos, e avanços em uma das frentes frequentemente leva a progressos na outra. Restringindo a complexidade de passos de inferência dentro de uma prova, pode-se obter um fragmento da Aritmética de Peano chamado de Aritmética Cotada (Bounded Arithmetic), que define exatamente os predicados na hierarquia polinomial. Trabalhos recentes e bastante promissores têm mostrado que se certas teorias formais de aritmética cotada podem provar limites inferiores em teoria da complexidade, então os sistemas criptógraficos correspondentes não poderão ser seguros.