Семинары

Рассылка: https://groups.google.com/forum/#!forum/spb-algo



Амплификация сложности для некоммутативных арифметических схем

Докладчик: 
Иван Михайлин
Дата: 
Thursday, November 17, 2016 - 11:00
Место: 
ПОМИ, ауд. 402
Аннотация: 

Размер арифметических схем является одним из наиболее естественных мер сложности полиномов. Так как арифметические схемы обобщают булевы схемы, доказывать для них нижние оценки должно быть проще, поэтому доказательство суперполиномиальной нижней оценки на размер арифметических схем для явно заданного полинома будет очень неплохим
разогревом перед доказательством "NC_1 не содержит P". К сожалению, несмотря на многолетние изучение, прогресс в этом направление не внушает оптимизма.
Чтобы еще немного упростить вопрос, можно рассмотреть модель некоммутативных арифметических схем. Это звучит как очень хорошая идея, так как некоммутативные арифметические схемы является прямым обобщением обычных арифметических схем. К тому же для некоммутативных арифметических формул мы знаем экспоненциальные нижние оценки. Однако
для схем не удалось получить никаких новых результатов. В докладе будет предложено объяснение, почему доказать суперлинейную нижнюю оценку может оказаться сложнее чем казалось изначально. А именно: такая оценка может быть амплифицированна до суперполиномиальной.



Миникурс по сложности пропозициональных доказательств. Ширина и размер резолюционных доказательств

Докладчик: 
Ицыксон Д.М. (ПОМИ РАН)
Дата: 
Friday, November 11, 2016 - 17:30
Место: 
ПОМИ, ауд. 203
Аннотация: 

Миникурс предназначен для студентов, аспирантов и всех интересующихся сложностью пропозициональных доказательств.
В первой лекции будет рассказано о резолюционной системе доказательств. В частности, мы изучим теорему Бен-Сассона и Вигдерсона о связи ширины и размера резолюционных доказательств. В качестве следствия будет приведены доказательства экспоненциальных нижних оценок на размер доказательства цейтинских формул и принципа Дирихле.



Автоматический логический вывод в интуиционистских логических исчислениях обратным методом Маслова

Докладчик: 
Павлов В.А. (СПбПУ)
Дата: 
Monday, November 7, 2016 - 14:00
Место: 
ПОМИ, ауд. 106
Аннотация: 

Рассматривается применение обратного метода Маслова для автоматического логического вывода в интуиционистской логике первого порядка. На данный момент существует немного программных реализаций обратного метода для этой логики, при этом остаётся пробел между теоретическими достижениями и их внедрением на практике.
Разработано новое исчисление обратного метода для интуиционистской логики первого порядка и стратегии логического вывода для этого исчисления.
Разработан алгоритм логического вывода с возможностью комбинирования стратегий, применимый к предложенному исчислению и к другим исчислениям обратного метода. На основе алгоритма разработана программа автоматического логического вывода WhaleProver.
Проведено экспериментальное сравнение используемых стратегий по ряду критериев, выявлена оптимальная комбинация стратегий.
Программа WhaleProver апробирована на обширной библиотеке задач ILTP версии 1.1.2. Всего программа решила 810 задач, что сопоставимо с результатами лучших аналогов. Решён ряд новых задач. Программу можно использовать для обучения или интегрировать в существующие системы искусственного интеллекта.



О теоретико-групповом обобщении теоремы Морса и Хедлунда

Докладчик: 
Светлана Пузынина (Институт Математики им. Л. С. Соболева)
Дата: 
Monday, October 31, 2016 - 14:00
Место: 
ПОМИ, ауд. 106
Аннотация: 

В классической работе 1938 года Морс и Хедлунд доказали, что всякое непериодическое бесконечное слово содержит как минимум n+1 подслово длины n. Более того, бесконечное слово содержит ровно n+1 подслово для каждой длины n, если и только если оно бинарное, непериодическое и сбалансированное, т.е. является словом Штурма. В докладе мы рассмотрим обобщение понятия сложности слов через действия групп и обсудим обобщения теоремы Морса и Хедлунда.


Pages