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?
cc.complexity-theory
complexity
proof-assistants
Samuel Schlesinger
fonte
fonte
Respostas:
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.)
fonte