DM Seminar

Discrete Mathematics Seminar

Семинар 21 июня 2002 года

Пятница, 21 июня, комната 106. Начало в 18:00.

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

Доклад по статье P.Parrilo
ИСПОЛЬЗОВАНИЕ ПОЛУОПРЕДЕЛЕННОГО ПРОГРАММИРОВАНИЯ ДЛЯ ПОИСКА ПОЛУАЛГЕБРАИЧЕСКИХ ДОКАЗАТЕЛЬСТВ
Полуалгебраические системы доказательств -- один из новых интересных и активно изучаемых классов систем пропозициональных доказательств. В статье описывается новый подход для определения разрешимости системы полиномиальных неравенств с использованием полуопределенного программирования.
Основная идея метода заключается в переформулировке задачи разложения полинома от многих переменных в сумму квадратов в полуопределенную программу. Также используются некоторые результаты из вещественной алгебраической геометрии.
Автором статьи предложен эффективный алгоритм нахождения доказательства ограниченной степени в Positivstellensatz. Методы, использованные в этом алгоритме, имеют приложение и к другим задачам.
Источник: P.Parrilo, "Semidefinite programming relaxations for semialgebraic problems", Preprint, 2001, 15.

Семинар 18 июня 2002 года

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

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

СУБЪЕКТИВНЫЙ ВЗГЛЯД НА СИСТЕМЫ АВТОМАТИЧЕСКОГО ВЫВОДА ТЕОРЕМ

Семинар 11 июня 2002 года

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

Докладчик: А. О. Слисенко (Paris).

РАЗРЕШИМЫЕ КЛАССЫ В ЛОГИКЕ, ОСНОВАННЫЕ НА КОНЕЧНОЙ ОПРОВЕРЖИМОСТИ И ВЫПОЛНИМОСТИ

Семинар 26 апреля 2002 года

Пятница, 26 апреля, комната 106. Начало в 18:00.

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

Доклад по статье A.Atserias, M.Bonet
ОБ АВТОМАТИЗАЦИИ МЕТОДА РЕЗОЛЮЦИЙ И СВЯЗАННЫХ С НЕЙ СИСТЕМ ДОКАЗАТЕЛЬСТВ
(продолжение)

Семинар 19 апреля 2002 года

Пятница, 19 апреля, комната 106. Начало в 18:00.

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

Доклад по статье A.Atserias, M.Bonet
ОБ АВТОМАТИЗАЦИИ МЕТОДА РЕЗОЛЮЦИЙ И СВЯЗАННЫХ С НЕЙ СИСТЕМ ДОКАЗАТЕЛЬСТВ
Создания эффективного алгоритма для доказательства тавтологичности -- одна из важнейших задач информатики. В статье описывается новый алгоритм для доказательств тавтологичности методом резолюций, основанный на системах доказательств Res(k), являющихся обобщениями метода резолюций. Доказывается, что полученный алгоритм не хуже других алгоритмов для метода резолюций, а во многих случаях экспоненциально лучше.
Также в этой статье исследуется "слабая автоматизируемость" резолюционной системы доказательств, то есть, являются ли автоматизируемыми системы, полиноминально моделирующие метод резолюций. Эта проблема сводится к вопросу о существовании интерполянтов в системе доказательств Res(2).
В качестве побочного результата построен новый класс тавтологий, имеющих короткие доказательства методом резолюций, но обладающих при этим большой "шириной". Таким образом, снимается вопрос Алехновича и Разборова об автоматизации метода резолюций за квазиполиномиальное время.
Источник: A.Atserias, M.Bonet, "On the Automatizability of Resolution and Related Propositional Proof Systems", ECCC TR02-010.

Семинар 5 апреля 2002 года

Пятница, 5 апреля, комната 106. Начало в 18:00.

Докладчик: Ю. Лифшиц.

СВЯЗЬ КОНЕЧНЫХ АВТОМАТОВ С РЕГУЛЯРНЫМИ ВЫРАЖЕНИЯМИ ЗАДАЧА ОБ УНИВЕРСАЛЬНОМ ГРАФЕ
Эта задача возникла в теории конечных автоматов. Известно, что для языка каждого регулярного выражения существует конечный автомат, который этот язык распознает. При попытке дать нижнюю оценку количества переходов в этом автомате Hagenah и Muscholl сформулировали следущий результат:
Количество переходов в конечном недетерминированном автомате без пустых переходов, который распознает регулярный язык из $ n $ букв -- не меньше, чем количество ребер в Универсальном графе (УГ).
В той же статье получена и верхняя оценка:
Для любого регулярного выражения, построенного за $ n $ шагов, можно построить недетерминированный конечный автомат без пустых переходов, который будет распознавать язык этого выражения и содержать не более чем $ С n log^2 n $ переходов.
Таким образом, цель настоящей работы -- получить нижнюю оценку на количество ребер в УГ. Оценка, полученная в работе Hagenah и Muscholl -- $ c n log n $. Результат настоящей работы -- нижняя оценка $ c_1 n log^2 n/log log n $. Основная идея доказательства -- переход от ориентированного графа к стрелочным структурам. Однако, по мнению автора, таким путем невозможно получить оценку $ c_2 n log^2 n $.

Семинар 15 марта 2002 года

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

Докладчик: Б. Ф. Мельников (Ульяновский гос.университет).

ПРОСТОЕ РЕШЕНИЕ ПРОБЛЕМЫ ЗВЕЗДНОЙ ВЫСОТЫ (Часть I)
Проблема звездной высоты регулярного языка была поставлена в самом начале 1960-х годов и очень долгое время оставалась нерешенной. Кратко сама проблема может быть сформулирована следующим образом: определяем звездную высоту (ЗВ) регулярного выражения (РВ) как максимальное вложение в нем операции "звезда"; известно, что для каждого регулярного языка (РЯ) существует бесконечно много РВ, определяющих этот язык; существует ли алгоритм, определяющий, какое именно из этих РВ имеет минимальную ЗВ? В 1987-м году вышла пока единственная публикация с довольно сложным алгоритмом, решающим данную проблему (K.Hashiguchi).
Автор данных тезисов предлагает значительно более простое решение, базирующееся на построении специальных недетерминированных конечных автоматов (КА). Данное решение является продолжением серии работ автора, связанных с исследованием РЯ с помощью т.н. функций разметки состояний КА; в тех работах, среди прочих, были решены задачи минимизации КА по другим критериям - вершинной и дуговой.
Вторая часть доклада состоится на заседании семинара лаборатории математической логики ПОМИ в понедельник, 18 марта в 14:00, к.203.

Семинар 1 марта 2002 года

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

Докладчик: Э. Гирш (совместная работа с Д.Григорьевым и Д.Пасечником).

ПОЛУАЛГЕБРАИЧЕСКИЕ ДОКАЗАТЕЛЬСТВА
Вывод пропозициональной тавтологии в полуалгебраической системе доказательств заключается в опровержении некоторой системы полиномиальных неравенств. Эти системы являются довольно сильными: в них имеются короткие доказательства принципа Дирихле, Цейтинских тавтологий, нераскрашиваемости k-клики в (k-1) цвет и т.д. Тем не менее, для наиболее слабых из полуалгебраических систем получены экспоненциальные нижние оценки на длину вывода.

Семинар 8 февраля 2002 года

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

Докладчик: В. Б. Балакирский (EIDMA, Eindhoven University of Technology).

HASHING OF DATABASES WITH THE USE OF METRIC PROPERTIES OF THE HAMMING SPACE
We describe hashing of databases as a problem of information and coding theory. It is shown that the triangle inequality for the Hamming distances between binary vectors can essentially decrease the computational efforts of searching for a pattern in databases. Introduction of the Lee distance in the space, which consists of the Hamming distances, leads to a new metric space where the triangle inequality is effectively used.

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

Пятница, 28 декабря, комната 106. Начало в 18:00.

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

УНИФИКАЦИЯ И ЕЕ ПРИЛОЖЕНИЯ К ПРОБЛЕМЕ РАЗРЕШИМОСТИ
Унификация (unification) -- это подстановка в два терма вместо переменных других термов, так чтобы получившиеся термы совпали. Естественно, это возможно не для любых двух термов. В докладе приводится алгоритм, работающий за полиномиальное время, проводящий унификацию. В алгоритме используются ориентированные графы без циклов (dag). Дается оценка на сложность задачи унификации. Из этой оценки, в свою очередь, следует оценка на сложность проблемы разрешимости для Эрбрановских формул.

Syndicate content