Формально проверенная теория сложности

18

Существует ли какой-либо текущий проект по формальной проверке теорем и доказательств теории сложности с использованием помощника по доказательствам, такого как Coq? Есть ли границы для этого?

cc.complexity-theory complexity proof-assistants Сэмюэль Шлезингер
источник
3
Я думаю, что некоторые исследования проводятся в Болонском университете с ассистентом Matita. См., Например, Формализация машин Тьюринга .
Марцио Де
Связанный: cstheory.stackexchange.com/q/4052/129 . Некоторые ответы даже говорят о Coq, а другие упоминают результаты, которые можно интерпретировать как теоретические барьеры для этого проекта, хотя, вероятно, они не являются барьерами на практике.
Джошуа
Спасибо, этот вопрос был замечательным @JoshuaGrochow, я так рада, что узнала об этой монографии Хартманниса. Если я понимаю, барьером было бы убедиться, что определяемые вами классы сложности - это то, что, по вашему мнению, является версией, а не «доказуемостью в Coq».
Самуэль Шлезингер
1
Там в ответ на аналогичный вопрос здесь , хотя это больше о доказательстве конкретных оценок сложности , чем результаты общей теории сложности
jmite
Да, это актуально, хотя. Мне любопытно, как может помочь базовая система типов, например, включить некоторые понятия сложности в типы функций. Конечно, это привело бы к широкому диапазону равенств, но я думаю, что это то, что мы имеем в сложности, естественно, в любом случае.
Самуэль Шлезингер

Ответы:

6

В следующей статье мой коллега Ули Шёпп представляет формальную проверку (в Coq) нетривиального результата Кука и Рэкоффа на вычислительную мощность графовых автоматов. https://scholar.google.at/scholar?oi=bibs&cluster=4944920843669159892&btnI=1&hl=de (Schöpp, U. (2008). Формализованная нижняя граница достижимости неориентированного графа. В логике для программирования, искусственного интеллекта и рассуждения ( С. 621-635). Спрингер Берлин / Гейдельберг.)

Мартин Хофманн
источник
1
Не могли бы вы дать полную ссылку, чтобы ответ не зависел от действительности ссылки?
Holf