Сложность доказательства
-
Определение и сложность доказательства
- Доказательство — это процесс, который демонстрирует истинность утверждения.
- Сложность доказательства — это количество шагов, необходимых для его создания.
-
Системы доказательств и их сложность
- Системы доказательств классифицируются по сложности и эффективности.
- Системы доказательств P включают арифметику высказываний и логику высказываний.
- Системы доказательств NP включают арифметику высказываний и логику высказываний с полиномиальным временем проверки.
-
Методы доказательства и их эффективность
- Метод резолюции использует логические правила для доказательства тавтологий.
- Метод DPLL использует поиск с возвратом для доказательства тавтологий.
- Системы доказательств с ограниченной глубиной, такие как система Фреге, имеют экспоненциальные нижние границы сложности.
-
Нижние границы и выполнимая интерполяция
- Нижние границы доказывают, что некоторые задачи не могут быть решены за полиномиальное время.
- Выполнимая интерполяция позволяет эффективно вычислять интерполирующие схемы из доказательств тавтологий.
-
Связь между автоматизацией и сложностью доказательства
- Слабая автоматизируемость системы доказательств подразумевает возможность выполнимой интерполяции.
- Некоторые системы доказательств, такие как расширенная система Фреге, не могут быть слабо автоматизируемы без защиты от определенных атак.
-
Неклассическая логика и размер доказательств
- В неклассической логике, например, интуиционистской и модальной, были получены экспоненциальные нижние границы размера доказательств.
-
Рекомендации и дальнейшее чтение
- Статья предлагает список литературы и внешних ссылок для дальнейшего изучения темы.
Полный текст статьи: