Существует ли разумная автоматизированная система доказательств для теорем TCS?

28

Предположим, я хотел формализовать доказательство Тьюринга относительно проблемы остановки, чтобы машина могла его проверить. Некоторые из известных автоматизированных систем доказательства теорем включают Mizar, Coq и HOL4. Я скачал и экспериментировал с Coq, но у него нет библиотеки для машин Тьюринга. Я думал сам написать один код, но обнаружил, что учебника не хватает, а язык трудно подобрать.

Мой вопрос таков: есть ли автоматический доказатель теорем, который, как правило, хорошо доказывает теоремы, связанные с машинами Тьюринга? Я бы посчитал такой доказатель теоремы «хорошим», если бы он мог формализовать доказательство неразрешимости проблемы остановки, используя уже существующие библиотеки. Я бы посчитал это еще лучше, если его относительно легко подобрать. (Кстати, у меня обычно нет проблем с языками программирования.)

Благодарность,

Филипп

lo.logic turing-machines software proof-assistants automated-theorem-proving Филип Уайт
источник
Вы можете проверить эту страницу, но в список не входит проблема остановки.
Каве
10
Я осмелюсь сказать, что вам нужно упорствовать с чем-то вроде Coq, прежде чем это станет естественным. И вы должны быть в терминале, работая над проблемами, а не читать книгу. Попадание в руки «Интерактивного доказательства теорем и разработки программы: Coq'Art: исчисление индуктивных конструкций» поможет. Уроки Coq: cis.upenn.edu/~bcpierce/sf и adam.chlipala.net/cpdt довольно хороши (хотя и не направлены непосредственно на то, что вы хотите).
Дэйв Кларк
5
Формализация доказательства может быть довольно сложной, если вы выберете «неправильную» его версию. Для проблемы Остановки я бы предложил сначала доказать более общую и абстрактную версию. Позже вы можете доказать, что машины Тьюринга являются частным случаем абстрактной версии, если вам все еще хочется делать это (будет очень много нудных подробностей о машинах Тьюринга, так что, возможно, лучше было бы потратить время на то, чтобы заняться чем-то другим). Я подумаю о хорошем способе доказать это в Coq. Оставайтесь с нами.
Андрей Бауэр
5
Если вы хорошо разбираетесь в математике и умеете программировать, у вас есть предпосылки, чтобы научиться пользоваться ассистентом. Вы действительно должны относиться к нему как к новому навыку. (Это, однако, очень полезно.)
Нил Кришнасвами
Похоже, ответ на вопрос «нет». Я думаю, что такая система была бы очень полезна - могу ли я попросить, чтобы, если вы действительно формализуете машины Тьюринга, не могли бы вы немного подумать об эквивалентности за полиномиальное время?
Колин Маккуиллан

Ответы:

17

Вот библиотека Изабель / HOL, содержащая теорему Райса, которая заявляет о неразрешимости широкого круга задач. Поскольку эта библиотека моделирует вычислимость с помощью рекурсивных функций, вы должны закодировать универсальную машину Тьюринга как рекурсивную функцию, чтобы использовать эту теорему для доказательства неразрешимости проблемы остановки машин Тьюринга. Однако существенные части доказательства неразрешимости уже сделаны.

http://afp.sourceforge.net/browser_info/current/HOL/Recursion-Theory-I/index.html

yhirai
источник