Laboratory of Mathematical Logic at PDMI

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

Докладчик: С. Николенко, А. Сироткин.

Тема: Автоматические доказательства верхних оценок для DPLL-подобных алгоритмов.

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

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

Тема: Formal Verification of the VAMP Floating Point Unit.

Пятница, 7 февраля, комната 101. Начало в 16:30.

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

Тема: Теория К-связных графов. Новые результаты.

Пятница, 27 декабря, комната 106. Начало в 16:30.

Докладчик: Ю. В. Матиясевич.

AN EASY TO UNDERSTAND PROOF OF TARSKI'S THEOREM ON THE DECIDABILITY OF THE THEORY OF REAL NUMBERS
I will present a proof of the famous theorem from the title which 1) is easy to understand; 2) is easy to implement 3) but the resulting algorithm is very inefficient, alas!
My presentation will be based on the talk given by Hoon Hong at ACA'2002 with some improvements.

Пятница, 20 декабря, комната 106. Начало в 16:30.

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

СТАРЫЕ и НОВЫЕ МЕТОДЫ АВТОМАТИЧЕСКОГО ПОИСКА ДОКАЗАТЕЛЬСТВ (четвертое продолжение)
ВНИМАНИЕ: доклад будет продолжаться в два раза дольше обычного.

Воскресенье, 15 декабря, комната 106. Начало в 16:30.

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

СТАРЫЕ и НОВЫЕ МЕТОДЫ АВТОМАТИЧЕСКОГО ПОИСКА ДОКАЗАТЕЛЬСТВ (третье продолжение)

Пятница, 6 декабря, комната 106. Начало в 16:30.

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

СТАРЫЕ и НОВЫЕ МЕТОДЫ АВТОМАТИЧЕСКОГО ПОИСКА ДОКАЗАТЕЛЬСТВ (второе продолжение)

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

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

Доклад по статье E.Balas, S.Ceria, G.Cornuejols
A LIFT-AND-PROJECT CUTTING PLANE ALGORITHM FOR MIXED 0-1 PROGRAMS
Abstract _статьи_:
We propose a cutting plane algorithm for mixed 0-1 programs based on a family of polyhedra which strengthen the usual LP relaxation. We show how to generate a facet of a polyhedron in this family which is most violated by the current fractional point. This cut is found through the solution of a linear program that has about twice the size of the usual LP relaxation. A lifting step is used to reduce the size of the LP's needed to generate the cuts. An additional strengthening step suggested by Balas and Jeroslow is then applied. We report our computational experience with a preliminary version of the algorithm. This approach is related to the work of Balas on disjunctive programming, the matrix cone relaxations of Lovasz and Schrijver and the hierarchy of relaxations of Sherali and Adams.

Пятница, 29 ноября, комната 106. Начало в 16:30.

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

СТАРЫЕ и НОВЫЕ МЕТОДЫ АВТОМАТИЧЕСКОГО ПОИСКА ДОКАЗАТЕЛЬСТВ (продолжение)
Будет описано дерево поиска опровергающих моделей.

Пятница, 22 ноября, комната 106. Начало в 16:30.

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

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