Цель этого вопроса - собрать примеры из теоретической информатики, где систематическое использование компьютеров было полезным
- в построении гипотезы, которая приводит к теореме,
- фальсификация гипотезы или доказательного подхода,
- построение / проверка (части) доказательства.
Если у вас есть конкретный пример, пожалуйста, опишите, как это было сделано. Возможно, это поможет другим более эффективно использовать компьютеры в своих ежедневных исследованиях (что на сегодняшний день все еще кажется довольно редкой практикой в TCS).
(Помечено как вики сообщества, поскольку нет единого «правильного» ответа.)
Ответы:
Очень известный пример - теорема о четырех цветах , первоначально доказанная исчерпывающей проверкой.
источник
Показывать, что проблема минимальной триангуляции (MWT) была NP-трудной, была давней открытой проблемой, осложненной тем фактом, что длины ребер включают в себя квадратные корни, и желаемую точность, необходимую для их точного вычисления, было трудно определить.
Малзер и Роте показали, что MWT был NP-hard , и в процессе использовали компьютерную помощь, чтобы проверить правильность своих гаджетов. Насколько я знаю, альтернативных доказательств нет.
источник
Доказательство Томаса Хейлса (его сайт, MathSciNet ) гипотезы Кеплера включало в себя так много анализа случаев - и случаи в свою очередь проверялись компьютером - что он решил попытаться получить формальное доказательство этого. Его проект для этого - FlysPecK , и он оценивает, что это займет 20 лет работы.
Исследователи языков программирования регулярно используют компьютерные доказательства в своей работе, хотя я не знаю, насколько это важно с точки зрения их исследовательского процесса (хотя это, безусловно, не дает им писать тонны утомительных манипуляций).
источник
Дорон Цайлбергер проделал определенную работу в области компьютерных доказательств. В частности, он подготовил программу Maple для доказательства геометрических тождеств и другую программу для доказательства класса комбинаторных тождеств . Некоторые из методов , которые упоминаются в книге A = B .
источник
Компьютеры также использовались для определения верхних границ времени выполнения программ обратного отслеживания, решающих сложные задачи NP, и создания гаджетов для подтверждения результатов неприемлемости. Эта и другие веселые темы ждут вас в коротком эссе (предупреждение, предельная самореклама), озаглавленном «Применение практики к теории». Смотрите http://arxiv.org/abs/0811.1305
Учитывая этот хороший список, похоже, я должен обновить статью!
источник
Контрпример к гипотезе Гирша , важный для линейного программирования и многогранной комбинаторики, был предложен Франциско Сантосом совсем недавно. Проверка компьютера была использована в первую очередь для установления некоторых свойств, требуемых в этом примере, хотя впоследствии были обнаружены аргументы без помощи вычислительной мощности, ср. Сообщение в блоге Гила Калаи или статья об архиве .
источник
Я не видел здесь упомянутого, но автоматическое средство проверки теорем решило давнюю открытую проблему того, являются ли алгебры Роббинса булевыми:
http://www.cs.unm.edu/~mccune/papers/robbins/
Это особенно примечательно, потому что компьютер разработал все доказательства, и проблема была открыта в течение нескольких десятилетий.
Не совсем уверен, что он квалифицируется как TCS, но, возможно, он тесно связан.
источник
Алгоритм Карлофф-Цвик для MAX-3sat достигает ожидается , производительность 7/8. Однако анализ основан на недоказанных сферических объемных неравенствах. Это неравенство было окончательно подтверждено с помощью компьютерных доказательств в другой статье Цвика .
Помимо доказательства Хейлса к гипотезе Кеплера, как упомянуто выше, доказательство к гипотезе Сота и к гипотезе Додекаэдра также автоматизировано.
источник
Вы можете проверить домашнюю страницу Shalosh B. Ekhad . Этот компьютер некоторое время публиковал статьи (обычно с соавторами).
источник
Кристиан Урбан использовал ассистента по доказательству Изабель, чтобы проверить, что одна из основных теорем в его докторской диссертации была фактически теоремой [1]. Используя ассистента, нужно было сделать несколько изменений, но результат в значительной степени выдержал.
Точно так же Урбан и Нарбу также обнаружили ошибки в ручном и бумажном доказательстве доказательства полноты Crary для проверки эквивалентности.
Meikle и Fleuriot формализовали Grundlagen Гильберта в Изабель и продемонстрировали, что, вопреки утверждениям Гильберта, он все еще полагался на свое интуицию, чтобы формализовать геометрию аксиоматическим образом (в его доказательстве были пробелы, полученные от Гильберта, предполагающего что-то о диаграммах) [3] ,
[1]: Пересмотр сокращения выреза: одно трудное доказательство действительно доказательство
[2]: формализация в доказательстве полноты номинальной Изабель Крэри для проверки эквивалентности
[3]: Формализация Грюндлагена Гильберта в Изабель / Изаре
источник
Результаты в « Геометрии деревьев бинарного поиска » Демейна, Хармона, Яконо, Кейна и Патрашку были разработаны с помощью программного обеспечения для тестирования различных схем начисления платы и построения оптимальных оценок для последовательностей с малым доступом. (И да, «ослы» - это правильный термин.)
источник
Н. Шанкар проверил (полностью и механически) доказательство Гёделем теоремы неполноты и теоремы Чёрча - Россера, используя доказательство теоремы Бойера - Мура. Есть книга, описывающая, как это было сделано.
источник
По словам Саймона Плуффа , формула алгоритма Бэйли-Борвейна-Плуффа для вычисления n-го бита Пи без вычисления каких-либо более значимых битов была обнаружена с использованием компьютерно-защищенных систем.
источник
Есть множество примеров в анализе средних случаев алгоритмов. Возможно, некоторые из самых ранних - это компьютерные эксперименты, которые привели к публикации в STOC 1984 «Некоторые неожиданные ожидаемые результаты поведения для упаковки бинов», выполненной Бентли, Джонсоном, Лейтоном, МакГеохом и МакГеохом.
источник