Доклад посвящён двум алгоритмам элиминации кванторов [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 посредством элиминации кванторов.