Teoria da complexidade formalmente verificada

18

Existe algum projeto em andamento para verificar formalmente os teoremas e as provas da teoria da complexidade usando um assistente de prova como Coq? Existem limites para fazer isso?

Samuel Schlesinger
fonte
3
Eu acho que algumas pesquisas estão sendo feitas na Universidade de Bolonha com o assistente de prova de Matita. Veja, por exemplo, Formalização de máquinas de Turing .
Marzio De Biasi
Relacionado: cstheory.stackexchange.com/q/4052/129 . Algumas das respostas até falam sobre Coq, e outras mencionam resultados que podem ser interpretados como barreiras teóricas para este projeto, embora provavelmente não sejam barreiras na prática.
Joshua Grochow
Obrigado, essa pergunta foi ótima @ JoshuaGrochow, tão feliz por ter aprendido sobre a monografia de Hartmann. Pelo que entendi, a barreira seria garantir que as classes de complexidade que você define sejam o que você pensa que são e não a versão "comprovável em Coq".
Samuel Schlesinger
1
Há uma resposta a uma pergunta semelhante aqui , mas é mais sobre provando limites de complexidade específicos do que os resultados teoria da complexidade geral
jmite
Certo, isso é relevante. Estou curioso sobre as maneiras pelas quais o sistema de tipos subjacente pode ajudar, incluindo algumas noções de complexidade nos tipos de funções. Claro que isso levaria a uma ampla gama de igualdades, mas acho que é isso que temos em complexidade naturalmente de qualquer maneira.
Samuel Schlesinger

Respostas:

6

No artigo a seguir, meu colega Uli Schöpp apresenta uma verificação formal (em Coq) de um resultado não trivial de Cook e Rackoff sobre o poder computacional dos autômatos gráficos. https://scholar.google.at/scholar?oi=bibs&cluster=4944920843669159892&btnI=1&hl=de (Schöpp, U. (2008). Um limite inferior formalizado para a acessibilidade de gráficos não direcionados. Em lógica para programação, inteligência artificial e raciocínio ( 621-635). Springer Berlin / Heidelberg.)

Martin Hofmann
fonte
1
Você poderia, por favor, fornecer a referência completa para que a resposta não dependa da validade do link?
Holf