Михаил Романович Старчак - Докладчик

Доклад посвящён двум алгоритмам элиминации кванторов [1, 2], которые оперируют с экзистенциальными (∃-)формулами арифметики Бюхи Th⟨N;0,1,+,Vk, ≤⟩, где k ≥ 2 есть некоторое фиксированное натуральное число, а Vk есть двухместный предикат, истинный в точности для пар (x, y) ∈ N^2, таких что y есть наибольшая степень k, делящая x. В работе [1] впервые даётся полное описание множеств S ⊆ N, определимых с помощью ∃-формул арифметики Бюхи. До этого результата было известно лишь, что не все k-
регулярные предикаты являются ∃-определимыми [3]. Алгоритм элиминации кванторов из [1] пригоден и для доказательства принадлежности ∃Th⟨N;0,1,+,Vk, λx.2^x, ≤⟩ классу NExpTime. Однако, в результате совместной работы с Д. Чистиковым и А. Мансутти [2], удалось построить альтернативный алгоритм элиминации кванторов, который позволил доказать принадлежность указанной теории классу NP. Этот результат усиливает и обобщает принадлежность ∃-арифметики Бюхи классу NP [4] и ∃-арифметики
Семёнова классу NExpTime [5]. На пути построения разрешающей процедуры из класса NP было получено доказательство принадлежности классической задачи целочисленного линейного программирования классу NP посредством элиминации кванторов.
11 авг 2024

Событие (конференция)

ЗаголовокIV конференция математических центров России
Период6/08/2411/08/24
МестоположениеСанкт-Петербург
ГородСанкт-Петербург
Страна/TерриторияРоссийская Федерация
Степень признаниямероприятие национального масштаба без статуса международного мероприятия с участием мировых и/или национальных лидеров в данной области

ID: 131470744