DM Seminar

Discrete Mathematics Seminar

Семинар 23 марта 2001 года

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

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

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

Семинар 16 марта 2001 года

Пятница, 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 марта 2001 года

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

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

ЕЩЕ О ЧИСЛАХ КАРМАЙКЛА
В докладе улучшена оценка на число простых делителей строгого числа Кармайкла n-го порядка. Будет описан способ улучшения оценки для нестрогих чисел Кармайкла порядка n при малых n. Попутно доказывается оценка снизу на сумму $ \sum_{k=1}^n \phi(k) $.

Семинар 26 февраля 2001 года

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

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

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

Семинар 23 февраля 2001 года

Пятница, 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 февраля 2001 года

Вторник, 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 января 2001 года

Вторник, 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. Связь с нижними оценками для приближенных алгоритмов.

Семинар 16 января 2001 года

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

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

РАНГ МАТРИЦ И СЛОЖНОСТЬ ВЫЧИСЛЕНИЙ
Доклад представляет собой обзор статей B.Codenotti "Matrix rigidity" и B.Codenotti, G. Del Corso, Govanni Manzini "Matrix rank and communication complexity", посвященных связи между рангами некоторых матриц и сложности вычислений в линейной алгебре.

Семинар 5 декабря 2000 года

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

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

РАВЕНСТВА И ПЕРЕПИСЫВАНИЕ ТЕРМОВ
В докладе обсуждаются системы равенств и системы переписывания термов, некоторые их свойства (в частности, нетеровость, или остановочность) и связь этих свойств в проблемой разрешимости (теорема Кнута-Бендикса).

Семинар 28 ноября 2000 года

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

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

АВТОМАТИЧЕСКОЕ ПОРОЖДЕНИЕ ДОКАЗАТЕЛЬСТВ В СЕКВЕНЦИАЛЬНЫХ ИСЧИСЛЕНИЯХ С РАВЕНСТВОМ
(продолжение)

Syndicate content