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

    Области исследований

  • элиминация кванторов, экзистенциальная теория, делимость, алгоритмическая разрешимость, китайская теорема об остатках

ID: 86141154