Laboratory of Mathematical Logic at PDMI

Понедельник, 16 апреля, комната 412. Начало в 12:25.

Докладчик: Д. В. Карпов.

Состоится ПРОДОЛЖЕНИЕ
доклада по статье L.Lovasz STABLE SETS AND POLYNOMIALS.

Пятница, 13 апреля, комната 106. Начало в 17:00.

Докладчик: Д. В. Карпов.

Доклад по статье L.Lovasz
STABLE SETS AND POLYNOMIALS
Several applications of methods from nonlinear algebra to the stable set problem in graphs are surveyed. The most recent work cited was cowritten by A. Schrijver and involves nonlinear inequalities. These yield a procedure to generate facets of the stable set polytope. If a class of graphs has the property that all facets of the stable set polytope can be generated this way in a bounded number of steps, then the stable set problem is polynomially solvable for these graphs.

Пятница, 6 апреля, комната 106. Начало в 17:00.

Докладчик: Э. Гирш.

СОВРЕМЕННАЯ СТРУКТУРНАЯ ТЕОРИЯ СЛОЖНОСТИ
Доклад представляет собой обзор основных фундаментальных результатов 1980х-90х годов о взаимоотношениях между классами сложности вычислительных задач (P, NP, RP, BPP, BQP, PP, UP, ParityP, IP, PSPACE, ...).
Все необходимые определения будут приведены.

Пятница, 23 марта, комната 106. Начало в 17:00.

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

REDUCTION RULES AND UNIVERSAL VARIABLES FOR FIRST ORDER TABLEAUX AND DPLL
Упрощающие правила (редукции) играют большую роль в автоматическом поиске вывода. Хорошо известна их роль в пропозициональной логике; для логики первого порядка упрощающие правила применяются в основном для резолюционного исчисления. Используемые в исчислениях секвенциального типа "жесткие" переменные затрудняют применение упрощающих правил. Предлагается вариант редукций для секвенциальных исчислений первого порядка, вводимых благодаря "универсальным" переменным и правилу переименования.
Доклад подготовлен по одноименной статье Fabio Massacci.

Пятница, 16 марта, комната 101. Начало в 17:00.

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

A FIRST-ORDER DAVIS-PUTNAM-LOGEMANN-LOVELAND PROCEDURE
В докладе будет рассказано о Davis-Putnam-Logeman-Loveland (DPLL) procedure для первого порядка (FDPLL).
DPLL для пропозициональной логики представляет собой расщепление по контрарным литералам. FDPLL является обобщением DPLL, с расщеплением по неосновным (т.е., содержащим переменные) литералам.
В качестве преимуществ FDPLL приводятся скромные требования к памяти, наличие всего 2-х правил вывода и явное построение модели в случае, если опровержения формулы не существует.
Доклад основан на статье Peter Baumgartner "FDPLL - A First-Order Davis-Putnam-Logeman-Loveland Procedure".

Пятница, 2 марта, комната 412. Начало в 13:00.

Докладчик: О. Етеревский.

ЕЩЕ О ЧИСЛАХ КАРМАЙКЛА
В докладе улучшена оценка на число простых делителей строгого числа Кармайкла n-го порядка. Будет описан способ улучшения оценки для нестрогих чисел Кармайкла порядка n при малых n. Попутно доказывается оценка снизу на сумму .

Понедельник, 26 февраля, комната 412. Начало в 12:00.

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

ПРОДОЛЖЕНИЕ доклада
НИЖНИЕ ОЦЕНКИ ДЛЯ СИСТЕМ ФРЕГЕ С ОГРАНИЧЕННОЙ ГЛУБИНОЙ

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

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

НИЖНИЕ ОЦЕНКИ ДЛЯ СИСТЕМ ФРЕГЕ С ОГРАНИЧЕННОЙ ГЛУБИНОЙ
Состоится доклад по статье P.Beame, S.Riis "More on the relative strength of counting principles".
Будет доказана нижняя экспоненциальная оценка размера доказательства версии "на" принципа Дирихле (onto-PHP^{n+n^{\epsilon\log n}_n}) для систем Фреге с ограниченной глубиной (bounded-depth Frege) даже в случае, если в качестве схемы аксиом добавляются все "считающие" тавтологии Count_p (т.е. тавтологии, выражающие факт, что не существует совершенного разбиения множества из M элементов на блоки по p элементов, если M!=0 (mod p)).

Вторник, 6 февраля, комната 106. Начало в 11:59.

Докладчик: Э. Гирш.

ДОКАЗАТЕЛЬСТВО PCP THEOREM
Будет приведено доказательство первой (более простой) части PCP Theorem, иначе говоря, доказано, что для проверки выполнимости булевой формулы достаточно проверить всего лишь КОНСТАНТНОЕ количество битов "доказательства" (при этом разрешается использовать O(n^3) случайных битов).
Необходимые определения будут повторены (впрочем, они фактически содержатся в предыдущем абзаце).
Web-page семинара: http://logic.pdmi.ras.ru/~hirsch/minisem/ Подписка: email по адресу majordomo@logic.pdmi.ras.ru с командой SUBSCRIBE _minisem

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

Докладчик: Э. Гирш.

ВЕРОЯТНОСТНО ПРОВЕРЯЕМЫЕ ДОКАЗАТЕЛЬСТВА (PCP THEOREM)
Первый в серии докладов об одном из наиболее значительных достижений в структурной теории сложности 1990-х годов, положительно отвечающем на вопрос
"МОЖНО ЛИ ПРОВЕРИТЬ ДОКАЗАТЕЛЬСТВО, ПРОЧТЯ В НЕМ ЛИШЬ ТРИ БИТА?"
(Речь идет о доказательствах утверждений, принадлежащих классу NP.)
Язык принадлежит классу PCP(r(n),q(n)), если доказательство принадлежности к нему может быть проверено с использованием O(r(n)) случайных битов и O(q(n)) битов доказательства. Так называемая PCP Theorem гласит, что
NP = PCP(log n,1),
т.е., например, для вероятностной проверки выполнимости булевой формулы достаточно знать лишь КОНСТАНТНОЕ число (на самом деле, 3) битов доказательства. (Заметим, что определение NP требует проверки ВСЕХ битов доказательства.)
Содержание первого доклада: 1. Определения. 2. Дискуссия. 3. Связь с нижними оценками для приближенных алгоритмов.