Метод принуждения, использованный в работе Релятивизационной работы Бейкера-Гилла-Соловая и Доказательство Коэном независимости гипотезы Континуума

Меня вообще интересует метод принуждения, используемый Бейкером-Джиллом-Соловеем и Коэном. Я ищу столько источников, сколько смогу получить информацию о самой технике или ее использовании. У кого-нибудь есть предложения?

Подробнее о применении форсирования (через так называемые общие оракулы) в теории сложности см. Инструментарий Oracle Builder ( бесплатно доступен на домашней странице Fortnow ) от Fenner, Fortnow, Kurtz и Li. Они дают общую теорию общих оракулов и показывают ее многочисленные приложения в сложности.

Если вам интересно, как оракулы по сложности похожи на доказательства независимости в теории множеств, вас могут заинтересовать следующие статьи:

• Арора, Импальяццо, Вазирани. Релятивизирующие и нерелятивизирующие методы: роль локальной проверяемости .

• Импальяццо, Кабанец, Колоколова. Аксиоматический подход к алгебризации . ( полная версия свободно доступна на домашней странице Кабанца )

Об использовании принуждения в теории множеств см. Книгу Теории множеств ( Теория множеств на Амазонке ) Джека, особенно части II и III книги (не путать с «Введение в теорию множеств» Грбачека и Йеха).

Отличное введение в принуждение в теории множеств приведено в известной публикации USENET Тимоти Чоу «Форсирование для чайников», а также в более формальной статье «Руководство для начинающих по принуждению» .

Для использования методов принуждения в доказательной сложности вы можете посмотреть:

• М. Айтай. Сложность принципа голубя . В материалах 29-го ежегодного симпозиума IEEE по основам информатики, White Plains, NY, 1988, pp. 346–355; и

• М. Айтай. Сложность принципа голубя . Combinatorica 14 (1994), нет. 4, 417–433.

Метод доказательства является арифметическим аналогом принуждения (такого типа, который уже использовали Париж и Уилки). Более комбинаторные (и улучшенные нижние оценки) имеются в J. Krajıcek, P. Pudlak и A. Woods, Экспоненциальные нижние оценки на размер ограниченной глубины. Доказательства Фреге принципа голубиных ям, алгоритмы случайных структур, 7 (1995), pp. 15-39. T. Pitassi, PW Beame и R. Impagliazzo, Экспоненциальные нижние оценки для принципа голубя , Comput. Сложность, 3 (1993), с. 97–140.

Смотрите также:

• Миклос Айтай. Независимость по модулю Принципы счета$p$ . ECCC 1994.

• Сорен Риис. Финитизация в ограниченной арифметике . 1994, БРИКС, факультет компьютерных наук Орхусского университета.

Недавно Ян Крайчек опубликовал книгу, объединяющую эти методы принуждения:

• Я. Крайчек. Форсирование со случайными переменными и доказательство сложности . Издательство Кембриджского университета, декабрь 2010 г. ( Черновик доступен на домашней странице Крайчека )

см. также Принудительное доказательство в теории доказательств Avigad, 30pp, 2004. Он цитирует BGS75, но не подробно. есть некоторая ссылка на Скотта / Соловея как на перефразирование принуждения в булевозначные модели.

Идеи принуждения оказали влияние на вычислительную сложность; например, разделение классов сложности, относящихся к оракулу (например, как в BGS75), часто можно рассматривать как ограниченные ресурсами варианты форсирования.