Mathematical Logic and Discrete Mathematics at PDMI

Вторник, 18 апреля, комната 412. Начало в 13:30.

Докладчик: А. Тискин.

НЕСТАНДАРТНЫЕ ПРИМЕНЕНИЯ ЭКСТРЕМАЛЬНОЙ ТЕОРИИ ГРАФОВ
В 1975 г. Семереди сформулировал и доказал лемму о регулярном разбиении (Szemeredi's regularity lemma). В последние годы этот результат стал активно использоваться для решения экстремальных задач теории графов, однако его применение возможно и в других областях математики. В докладе будет рассказано о двух задачах, решенных при помощи нестандартного применения леммы семереди: задача об асимптотической плотности упаковки трехмерных полимино, и задача о коммуникационной сложности умножения булевых матриц.

Вторник, 4 апреля, комната 412. Начало в 15:00.

Докладчик: А. Косовская.

ОПИСАНИЕ ХРОМАТИЧЕСКОГО ЧИСЛА ГРАФА И ЧИСЛА НЕЗАВИСИМОСТИ С ПОМОЩЬЮ ПОЛИНОМА, ОПРЕДЕЛЯЕМОГО ГРАФОМ
Будут рассказаны связи между некоторым полиномом, задаваемым графом и числовыми характеристиками этого графа. отсюда выводятся некоторые оценки на число независимости графа. В частности, будут рассказаны результаты статьи L.Lovasz "Stable set and polynomials". Доклад тематически связан с докладом Д.Карпова и Ю.В.матиясевича 21 декабря 1999 года.

Вторник, 28 марта, комната 412. Начало в 14:00.

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

КВАНТОВЫЕ ВЫЧИСЛЕНИЯ С ТОЧКИ ЗРЕНИЯ ТЕОРИИ СЛОЖНОСТИ
Определяется класс вычислительных задач BQP (по аналогии с BPP). определение не несет "физической" терминологии, но охватывает все свойства квантовых вычислений. рассматривается место этого класса в общей картине сложностных классов.
Основной источник: L.Fortnow "One complexity theorist's view of quantum computing" (http://xxx.lanl.gov/abs/quant-ph/0003035)

Вторник, 21 марта, комната 412. Начало в 15:00.

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

ДОКАЗАТЕЛЬСТВА КАК ИГРЫ
доклад на основе статьи p.pudlak "proofs as games" (http://www.math.cas.cz/~pudlak/prfgame.ps)
Предлагается интересный способ получения нижней оценки (экспоненциальной) размера вывода pigeon hole principle методом резолюций. Вывод рассматривается как игра двух игроков: prover'а, который пытается получить противоречие из отрицания доказываемой формулы, и его оппонента, который пытается ему в этом помешать. В таких терминах нижняя оценка соответствует оптимальной стратегии оппонента.

Понедельник, 13 марта, комната 203. Начало в 14:30.

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

Доклад будет сделан на основе статьи Atserias, Galesi, Gavald`a
MONOTONE PROOFS OF THE PIGEON HOLE PRINCIPLE
Abstract of this paper: We study the complexity of proving the Pigeon Hole Principle (PHP) in a monotone variant of the Gentzen Calculus, also known as Geometric Logic. We show that the standard encoding of the PHP as a monotone sequent admits quasipolynomial-size proofs in this system. This result is a consequence of deriving the basic properties of certain quasipolynomial-size monotone formulas computing the boolean threshold functions. Since it is known that the shortest proofs of the PHP in systems such as Resolution or Bounded Depth Frege are exponentially long, it follows from our result that these systems are exponentially separated from the monotone Gentzen Calculus. We also consider the monotone sequent (CLIQUE) expressing the clique-coclique principle defined by Bonet, Pitassi and Raz (1997). We show that monotone proofs for this sequent can be easily reduced to monotone proofs of the one-to-one and onto PHP, and so CLIQUE also has quasipolynomial-size monotone proofs. As a consequence, Cutting Planes with polynomially bounded coefficients is also exponentially separated from the monotone Gentzen Calculus. Finally, a simple simulation argument implies that these results extend to the Intuitionistic Gentzen Calculus. Our results partially answer some questions left open by P. Pudl'ak.
Full text: ftp://ftp.eccc.uni-trier.de/pub/eccc/reports/2000/TR00-008/index.html

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

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

ВОССТАНОВЛЕНИЕ ДОКАЗАТЕЛЬСТВ ПО СХЕМЕ В СЕКВЕНЦИАЛЬНЫХ ИСЧИСЛЕНИЯХ
Известно, что восстановление доказательства данной секвенции по схеме - алгоритмически неразрешимая задача для исчисления LK^{\Pi\Sigma} (стандартное секвенциальное исчисление в сечениями только по предваренным формулам с "однородным" кванторным префиксом: либо только кванторы всеобщности, либо только существования). Однако оказалось, что если в этом исчислении заменить правила введения квантора на правила введения произвольного числа кванторов, то такая задача становится разрешимой для древовидных доказательств. Результат тем более интересен, так как два упомянутых исчисления эквивалентны с точки зрения выводимости.

Cреда, 16 февраля, комната 106. Начало в 15:00.

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

БЛОЧНАЯ СТРУКТУРА $K$-СВЯЗНЫХ ГРАФОВ И УДАЛЕНИЕ ВЕРШИН БЕЗ ПОТЕРИ $K$-СВЯЗНОСТИ
В докладе будут изложены некоторые результаты относительно возможности удаления из $k$-связного графа вершин без потери $k$-связности. Также будет изложена конструкция, обобщающая разбиене связного графа на двусвязные блоки для случая $k$-связных графов.

Вторник, 8 февраля, комната 106. Начало в 15:00.

Докладчик: В. П. Оревков.

ПРЯМОЙ И ОБРАТНЫЙ МЕТОДЫ ПОИСКА ДОКАЗАТЕЛЬСТВ
В докладе будут описаны три варианта прямого (табличного) метода поиска доказательств в исчислении предикатов и построены соответствующие им варианты обратного метода. В частности, метод резолюций будет по этой схеме частным случаем обратного метода.

Вторник, 1 февраля, комната 106. Начало в 15:00.

Докладчик: М. А. Всемирнов.

ВВЕДЕНИЕ В ТЕОРИЮ КОДОВ (продолжение)
Доклад представляет собой обзор классических результатов в теории кодов. В частности, будет расказано о наиболее известных кодах и об их применении. Доклад основан на 3 главе книги Конвея и Слоана "Упаковки сфер, решетки и группы."

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

Докладчик: Г. В. Давыдов, И. М. Давыдова.

"О вычислении формул сечения при поиске вывода в исчислении предикатов"
Правило резолюций в методе резолюций Робинсона и правило Б в обратном методе Маслова являются правилами сечения по контрарной паре в первом случае и по исходной "clause" во втором. Выводом исходной формулы является вывод пустого объекта по этим правилам. В докладе предлагается, наоборот, по исходной формуле строить формулу сечения таким образом, что устранение сечения приводит к реконструкции исходных контрарных пар и исходных "clauses". Построенная формула сечения оказывается исходной для следующего шага. Последовательность формул сечения, оканчивающаяся пропозиционально выводимой формулой, является выводом исходной формулы.