¿Existe algún proyecto en curso para verificar formalmente los teoremas y las pruebas de la teoría de la complejidad utilizando un asistente de pruebas como Coq? ¿Hay límites para hacer esto?
cc.complexity-theory
complexity
proof-assistants
Samuel Schlesinger
fuente
fuente
Respuestas:
En el siguiente artículo, mi colega Uli Schöpp presenta una verificación formal (en Coq) de un resultado no trivial por parte de Cook y Rackoff sobre el poder computacional de los autómatas gráficos. https://scholar.google.at/scholar?oi=bibs&cluster=4944920843669159892&btnI=1&hl=de (Schöpp, U. (2008). Un límite inferior formalizado sobre accesibilidad gráfica no dirigida. En lógica para programación, inteligencia artificial y razonamiento ( pp. 621-635). Springer Berlin / Heidelberg.)
fuente