«Нелогические» доказательства для логических высказываний

Вопрос о наличии доказательства некоторого утверждения в логике высказываний — один из самых (вычислительно) «простых» в теории доказательств. Тем не менее, он очень важен, поскольку имеет непосредственное отношение к знаменитому вопросу о равенстве классов P и NP вычислительных задач (одному из семи вопросов, за решение которых Clay Mathematics Institute объявил приз в \$1,000,000). Именно, если не существует системы доказательств для логики высказываний, в которой для каждого истинного утверждения имеется доказательство полиномиального размера, то NP!=co-NP, а значит, P!=NP.
Естественно, ни для одной из известных систем доказательств подобного факта не известно, хотя для некоторых из них, наоборот, известны экспоненциальные нижние оценки. В последнее время, наряду с «чисто логическими» системами доказательства широкое внимание уделяется и другим системам, например, «алгебраическим» (рассуждения производятся над полиномами, а не над логическими формулами). Неожиданные системы возникают также при удалении использования случайных битов из вероятностных алгоритмов: применяемые для этого конструкции используют теорию кодирования и проективную геометрию.
Доклад будет посвящен обзору различных систем доказательств для логики высказываний.