Mathematical Logic and Discrete Mathematics at PDMI

Вторник, 22 февраля, комната 106. Начало в 17:00.

Докладчик: В. Жижкун.

ВОССТАНОВЛЕНИЕ ДОКАЗАТЕЛЬСТВ ПО СХЕМЕ В СЕКВЕНЦИАЛЬНЫХ ИСЧИСЛЕНИЯХ
Известно, что восстановление доказательства данной секвенции по схеме - алгоритмически неразрешимая задача для исчисления LK^{\Pi\Sigma} (стандартное секвенциальное исчисление в сечениями только по предваренным формулам с "однородным" кванторным префиксом: либо только кванторы всеобщности, либо только существования). Однако оказалось, что если в этом исчислении заменить правила введения квантора на правила введения произвольного числа кванторов, то такая задача становится разрешимой для древовидных доказательств. Результат тем более интересен, так как два упомянутых исчисления эквивалентны с точки зрения выводимости.

Cреда, 16 февраля, комната 106. Начало в 15:00.

Докладчик: Д. В. Карпов, А. В. Пастор.

БЛОЧНАЯ СТРУКТУРА $K$-СВЯЗНЫХ ГРАФОВ И УДАЛЕНИЕ ВЕРШИН БЕЗ ПОТЕРИ $K$-СВЯЗНОСТИ
В докладе будут изложены некоторые результаты относительно возможности удаления из $k$-связного графа вершин без потери $k$-связности. Также будет изложена конструкция, обобщающая разбиене связного графа на двусвязные блоки для случая $k$-связных графов.

Вторник, 8 февраля, комната 106. Начало в 15:00.

Докладчик: В. П. Оревков.

ПРЯМОЙ И ОБРАТНЫЙ МЕТОДЫ ПОИСКА ДОКАЗАТЕЛЬСТВ
В докладе будут описаны три варианта прямого (табличного) метода поиска доказательств в исчислении предикатов и построены соответствующие им варианты обратного метода. В частности, метод резолюций будет по этой схеме частным случаем обратного метода.

Вторник, 1 февраля, комната 106. Начало в 15:00.

Докладчик: М. А. Всемирнов.

ВВЕДЕНИЕ В ТЕОРИЮ КОДОВ (продолжение)
Доклад представляет собой обзор классических результатов в теории кодов. В частности, будет расказано о наиболее известных кодах и об их применении. Доклад основан на 3 главе книги Конвея и Слоана "Упаковки сфер, решетки и группы."

Вторник, 18 января, комната 106. Начало в 15:00.

Докладчик: Г. В. Давыдов, И. М. Давыдова.

"О вычислении формул сечения при поиске вывода в исчислении предикатов"
Правило резолюций в методе резолюций Робинсона и правило Б в обратном методе Маслова являются правилами сечения по контрарной паре в первом случае и по исходной "clause" во втором. Выводом исходной формулы является вывод пустого объекта по этим правилам. В докладе предлагается, наоборот, по исходной формуле строить формулу сечения таким образом, что устранение сечения приводит к реконструкции исходных контрарных пар и исходных "clauses". Построенная формула сечения оказывается исходной для следующего шага. Последовательность формул сечения, оканчивающаяся пропозиционально выводимой формулой, является выводом исходной формулы.

Понедельник, 10 января, комната 203. Начало в 14:30.

Докладчик: Б. Ю. Конев.

"Подход Г.Чайтина к колмогоровской сложности"
Этот подход отличается тем, что, в частности, предлагается ограничиться только такими программами универсальной машины Тьюринга, для которых никакой префикс не является программой (self-delimiting programs). Это позволяет ввести вероятность остановки $\Omega$ (halting probability). Будут рассмотрены свойства введенных понятий, а также следствия для алгоритмической теории информации.

Вторник, 28 декабря, комната 106. Начало в 18:00.

28 декабря.
М.А.Всемирнов "Реберные раскраски графов, Nullstellensatz и вычисление определителей".
Предлагается новый критерий существования реберных k-раскрасок графов, формулируемый в терминах обращения в 0 определителей специального вида. Тематически этот доклад связан с предыдущим докладом Д.В.Карпова и Ю.В.Матиясевича, однако изложение носит независимый характер.

Вторник, 21 декабря, комната 106. Начало в 18:00.

21 декабря.
Д.В.Карпов, Ю.В.Матиясевич
В первой части Д.В.Карпов изложит по статье N. Alon "Combinatorial Nullstelensatz" (Combinatorics Probability and Computing 1999, N8, p7-29) технику сведения комбинаторных проблем (в частности, связанных с раскрасками графов) к вопросам о нулях многочленов.
Во второй части семинара Ю.В.Матиясевич изложит результаты о связи существования правильной раскраски ребер триангуляции сферы и невырожденности специального полинома, соответствующего этому графу. (См. Homepage Ю.В.Матиясевича http://logic.pdmi.ras.ru/~yumat/ и статью Ю.В.Матиясевича "Один критерий раскрашиваемости вершин графа, формулируемый в терминах ориентации ребер" (Дискретный анализ, N26(1974) )

Вторник, 14 декабря, комната 106. Начало в 18:00.

14 декабря.
Э.Гирш "Сложность по Колмогорову: неожиданные примеры применения"
С помощью сложности по Колмогорову и _элементарной_ теории чисел будут заново (более просто) доказаны следующие результаты:
-- Valiant-Vazirani lemma о сведении SAT к SAT для одновыполнимых формул; -- Sipser's lemma; -- BPP \subset \Sigma_2^p.
Попутно получаются другие интересные результаты о ресурсно-ограниченной сложности по Колмогорову.
Доклад будет сделан на основе статьи H. Buhrman, L. Fortnow, "Resource-Bounded Kolmogorov Complexity Revisited", STACS-97.

Вторник, 30 ноября, комната 106. Начало в 18:00.

30 ноября.
В.Жижкун "Представление булевых функций ациклическими направленными графами"
АБСТРАКТ
Binary Decision Diagrams (BDDs) - способ представления логических функций, позволяющий эффективно реализовать различные операции над ними. В том, что такая проблема достаточно актуальна, можно убедиться, например, построив КНФ отрицания формулы в КНФ. Преимущество BDD в том, что результаты операций над булевыми формулами представляются компактно.
Кроме того, BDD - каноническая форма, поэтому проверка двух функций на эквивалентность заключается в сравнении двух направленых ациклических размеченых графов, а выполнимость формулы - сравнение соответствующего графа с тривиальным.
Существенный недостаток этого способа - необходимость фиксировать порядок переменных. Кроме того, размер графов существенно зависит от выбора такого порядка. Помимо этого, известно, что представление функции умножения двоичных чисел с помощью BDD требует экспоненциального числа узлов при любой перестановке переменных.
Доклад будет сделан на основе статьи Randal E. Bryant "Graph-Based Algorithms for Boolean Function Manipulation".