Вторник, 1 февраля, комната 106. Начало в 15:00.
Докладчик: М. А. Всемирнов.
ВВЕДЕНИЕ В ТЕОРИЮ КОДОВ (продолжение)Вторник, 18 января, комната 106. Начало в 15:00.
Докладчик: Г. В. Давыдов, И. М. Давыдова.
"О вычислении формул сечения при поиске вывода в исчислении предикатов"Понедельник, 10 января, комната 203. Начало в 14:30.
Докладчик: Б. Ю. Конев.
"Подход Г.Чайтина к колмогоровской сложности"Вторник, 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".
Вторник, 23 ноября, комната 106. Начало в 18:00.
23 ноября.
Д.В.Карпов, доклад по статье
D.Achlioptas, M.Molloy "Almost all graphs with 2.522N edges are not 3-colorable". (The Electronic Journal of Combinatorics, 6(1999), #R29)
Abstract. B этой работе доказывается, что для любого с>=2.522, вершины случайного графа с N вершинами и 2.522N ребрами нельзя правильным образом раскрасить в три цвета с вероятностью 1-o(1). Также в этой работе рассматтривается рассматривается аналогичный вопрос для k-раскрашиваемости при k>3, приводятся соответствующие оценки.
Вторник, 16 ноября, комната 106. Начало в 18:00.
16 ноября.
Б.Ю.Конев. Доклад о патентованном алгоритме Stalmark'а установления тавтологичности пропозициональных формул. Судя по результатам машинных тестов, алгоритм является достаточно эффективным, авторы утверждают, что время его работы зависит не от количества неизвестных, а от "логической структуры формулы". Алгоритм достаточно прост, но никаких оценок для него не известно. Доклад будет сделан на основе статьи John Harrison "Stalmark's Algorithm as a HOL Derived Rule", однако, детали реализации освещаться не будут.
Вторник, 2 ноября, комната 106. Начало в 18:00.
2 ноября.
В.Жижкун "Разрешимые частные случаи задачи квазиунификации".
АБСТРАКТ
Задача квазиунификации возникает естественным образом в теории логического вывода при при изучении возможности обобщения доказательств (гипотеза Крайзеля). В общей постановке задача оказывается алгоритмически неразрешимой. В докладе будет приведен общий (естественно, неполный) алгоритм ее решения, а также полные алгоритмы для двух частных случаев, имеющих конкретное применение в теории вывода. Эти алгоритмы позволяют получить верхние оценки высоты термов в решении.