Рассматривается применение обратного метода Маслова для автоматического логического вывода в интуиционистской логике первого порядка. На данный момент существует немного программных реализаций обратного метода для этой логики, при этом остаётся пробел между теоретическими достижениями и их внедрением на практике.
Разработано новое исчисление обратного метода для интуиционистской логики первого порядка и стратегии логического вывода для этого исчисления.

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

We present three results on the complexity of Minimax Approval Voting that is a voting rule for choosing committee of fixed size k. Here, we see the votes and the choice as 0-1 strings of length m (characteristic vertors of the subsets). The goal is to minimize the maximum Hamming distance to a vote. First, we study Minimax Approval Voting parameterized by the Hamming distance d from the solution to the votes. We show Minimax Approval Voting admits no algorithm running in time O*(2^o(d\log d)), unless the Exponential Time Hypothesis (ETH) fails.

Мы продолжим изучать информационно-сложностной подход к нижней оценке на сложность KW(f o U_n)

Вычисление наибольшей общей подпоследовательности (longest common subsequence, LCS) двух заданных строк - фундаментальная алгоритмическая задача, традиционно решаемая методом динамического программирования. Мы рассматриваем альтернативный метод решения типа divide-and-conquer, основанный на обобщении этой задачи, вычисляющем неявные матрицы полулокальных LCS. Решения на подзадачах "склеиваются" при помощи эффективного умножения в "моноиде водорослей", тесно связанном с классической группой кос.

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