Понятие стабильной модели формулы исчисления высказываний служит основой новой формы декларативного программирования, которая часто применяется сегодня для решения переборных задач. Мы рассмотрим примеры программ этого типа, написанных в языке системы CLINGO, созданной в Потсдамском университете в Германии. Затем мы обсудим два конкурирующих определения стабильной модели, используемые разными группами программистов, и новые результаты, описывающие, при каких условиях эти определения эквивалентны.

Due to the efforts of Fermat, Euler, Legendre and Gauss, it is known what
natural numbers can be written as the sum of two squares or three squares.
Lagrange's four-square theorem proved in 1770 states that each natural
number can be expressed as the sum of four squares.
In the talk we will first review classical results on sums of two or three
or four squares. Then we turn to the speaker's recent discoveries which
refine Lagrange's four-square theorem or the Gauss-Legendre theorem on
sums of three squares.
In particular we will introduce our results refining Lagrange's
four-square theorem as well as some recent conjectures of the speaker one
of which states that any integer greater than one can be written as the
sum of two squares, a power of 3 and a power of 5.

Монотонные Span Programs (mSP) были предложены Карчмером и Вигдерсоном в начале 90-х годов, позднее было
доказано, что они моделируют монотонные булевы формулы. Также известно квазиполиномиальное разделение между
mSP над полем F_2 и монотонными схемами.

Пользуясь недавними теоремами о лифтинге мы покажем, что задача о разделении данных моделей вычислений следует из разделения резолюционной системы доказательств и Nullstellensatz. Мы предъявим экспоненциальное разделение данных систем.