20 ноября 2000 г. Э.А.Гирш `Нелогические'' доказательства для логических высказываний.

Вопрос о наличии доказательства некоторого утверждения в логике высказываний -- один из самых (вычислительно) "простых" в теории доказательств. Тем не менее, он очень важен, поскольку имеет непосредственное отношение к знаменитому вопросу о равенстве классов P и NP вычислительных задач (одному из семи вопросов, за решение которых Clay Mathematics Institute объявил приз в $1,000,000). Именно, если не существует системы доказательств для логики высказываний, в которой для каждого истинного утверждения имеется доказательство полиномиального размера, то NP!=co-NP, а значит, P!=NP.

Естественно, ни для одной из известных систем доказательств подобного факта не известно, хотя для некоторых из них, наоборот, известны экспоненциальные нижние оценки. В последнее время, наряду с "чисто логическими" системами доказательства широкое внимание уделяется и другим системам, например, "алгебраическим" (рассуждения производятся над полиномами, а не над логическими формулами). Неожиданные системы возникают также при удалении использования случайных битов из вероятностных алгоритмов: применяемые для этого конструкции используют теорию кодирования и проективную геометрию.

Доклад будет посвящен обзору различных систем доказательств для логики высказываний.

Предыдущие заседания семинара: список докладов.