Seminars

Mailing list: https://groups.google.com/forum/#!forum/spb-algo



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

Speaker: 
Иван Михайлин
Date: 
Thursday, November 17, 2016 - 11:00
Place: 
ПОМИ, ауд. 402
Abstract: 

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



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

Speaker: 
Ицыксон Д.М. (ПОМИ РАН)
Date: 
Friday, November 11, 2016 - 17:30
Place: 
ПОМИ, ауд. 203
Abstract: 

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



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

Speaker: 
Павлов В.А. (СПбПУ)
Date: 
Monday, November 7, 2016 - 14:00
Place: 
ПОМИ, ауд. 106
Abstract: 

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



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

Speaker: 
Светлана Пузынина (Институт Математики им. Л. С. Соболева)
Date: 
Monday, October 31, 2016 - 14:00
Place: 
ПОМИ, ауд. 106
Abstract: 

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


Pages