Correspondência entre classes de complexidade e lógica

33

Tive uma vez aula sobre Computabilidade e Lógica. O material incluiu uma correlação entre as classes de complexidade / computabilidade (R, RE, co-RE, P, NP, Logspace, ...) e Lógica (cálculo de predicado, lógica de primeira ordem, ...).

A correlação incluiu vários resultados em um campo, que foram obtidos usando técnicas do outro campo. Foi suposto que P! = NP poderia ser atacado como um problema no Logic (projetando o problema do domínio das classes de complexidade para a lógica).

Existe um bom resumo dessas técnicas e resultados?

ripper234
fonte

Respostas:

23

É possível que você esteja perguntando sobre resultados na teoria de modelos finitos (como a caracterização de P e NP em termos de vários fragmentos da lógica). A recente tentativa de prova de P! = NP fez uso pesado de tais conceitos, e algumas boas referências (tiradas do wiki ) são

Suresh Venkat
fonte
Eu acho que o escopo da FMT é um pouco mais amplo do que apenas vincular lógica e complexidade computacional. Complexidade descritiva parece um termo mais preciso.
András Salamon
24

Neil Immerman produziu um belo diagrama que fornece correspondências imediatas entre classes de complexidade e lógicas interpretadas por modelos finitos. Está na capa de seu livro e também na parte inferior de sua página da web aqui: http://www.cs.umass.edu/~immerman/

Aaron Sterling
fonte
Esta imagem vale muitos milhares de palavras.
András Salamon
5
O livro de Immerman é provavelmente a melhor referência para os vínculos diretos entre lógica e complexidade computacional. Esse tópico geralmente é chamado de "Complexidade descritiva", como é o livro.
András Salamon
16

Conheço duas maneiras de associar lógica a classes de complexidade. O primeiro é a complexidade descritiva, que é a teoria do modelo mencionada em outras respostas. (Voltando à caracterização de por Ronald Fagin .)NP

A segunda abordagem (que também é um pouco mais antiga, remonta a trabalhos de pessoas como Steve Cook e Sam Buss) é a teoria da prova. Aqui, uma classe de complexidade é associada a teorias em aritmética. As funções comprovadamente totais dessas teorias são exatamente as funções da classe de complexidade. Por exemplo, funções comprovadamente totais da teoria de Sam Buss são exatamente funções computáveis ​​no tempo polinomial. Existem também links com sistemas de prova proposicional. Para saber mais sobre essa abordagem, consulte o livro de Jan Krajicek, "Aritmética limitada, lógica proposicional e teoria da complexidade", 1995, ou Stephen A. Cook e Phuong O livro mais recente de Nguyen, "Fundamentos lógicos da complexidade da prova", 2010 (um rascunho pode ser encontrado aqui ).S21

Antonina Kolokolova trabalhou nas relações entre essas duas abordagens.

Kaveh
fonte
11

Para aqueles que não estão familiarizados com a infinidade de acrônimos encontrados no grande diagrama de Immerman, há um artigo da Wikipedia sobre complexidade descritiva . Deve haver um diagrama com links, para que você possa procurar diretamente a definição no Complexity Zoo e outras fontes. Eu também gostaria de ver melhor as relações com as línguas / gramáticas formais correspondentes e onde você pode encontrar a prova.

Esta não é uma resposta, mas um comentário à resposta de Aarons, sobre a qual não posso comentar por algum motivo.

Jakob
fonte
você precisa de um pouco mais de representante para postar um comentário (é um mecanismo de bloqueio de spam).
Suresh Venkat