анная работа является первой частью нового доказательства разрешимости экзистенциальной теории структуры , где | соответствует двухместному отношению делимости. Разрешимость этой теории была доказана в 1976 г. независимо А.П. Бельтюковым и Л.Липшицем. В 1977 г. В. И.Мартьянов получил эквивалентный результат, рассматривая трехместный предикат НОД вместо отношения делимости (эти предикаты экзистенциально выражаются друг через друга с помощью других символов сигнатуры). В работе вводится понятие алгоритма квазиэлиминации кванторов (квази-ЭК), обобщающее в некотором смысле понятие алгоритма элиминации кванторов, а затем строится алгоритм квази-ЭК для позитивной экзистенциальной теории структуры <...>. К проблеме разрешимости для этой теории сводится проблема разрешимости для экзистенциальной теории структуры <...>. Алгоритм квази-ЭК, осуществляющий такое сведение, будет построен во второй части доказательства. Преобразования формул основаны на обобщении китайской теоремы об остатках для систем вида НОД(ai, bi + x) = di для всех i [1..m], где ai, bi, di - целые числа, такие что ai 6= 0, di > 0.
Original languageRussian
Pages (from-to)455-466
JournalВЕСТНИК САНКТ-ПЕТЕРБУРГСКОГО УНИВЕРСИТЕТА. МАТЕМАТИКА. МЕХАНИКА. АСТРОНОМИЯ
Volume8(66)
Issue number3
StatePublished - 26 Sep 2021

ID: 86141154