misle.ru страница 1
скачать файл
КОМПЬЮТЕРНАЯ ЛОГИКА

проф. С.Н. Артёмов

1. Интуиционистская логика, исходная доказуемостная семантика Брауэра-Гейтинга-Колмогорова. Система аксиом Гейтинга для интуиционистской логики. Топологическая модель интуиционистской логики, теорема Тарского о полноте. Модели Крипке, свойство монотонности, полнота.

2. Генценовские исчисления и естественный вывод, их эквивалентность гильбертовской системе. Алгоритмы перевода генценовских выводов в естественные и обратно. Нормальные формы. Теорема о нормализации (об устранении сечений) для интуиционистской логики.

3. Модальная логика и два типа семантики для модальности: “универсальная” (временная) и “экзистенциональная” (эпистемическая). Модели возможных миров Крипке для “универсальной” семантики. Генценовские системы для модальных логик K, K4, S4. Объединённая теорема о полноте для S4, доказывающая полноту по Крипке, устранение сечений, свойство конечности контрмоделей. Гёделевское сведение интуиционистской логики к модальной.

4. Простые типы как импликативный фрагмент интуиционистской логики. Типовая комбинаторная логика как исчисление доказуемостных термов для гильбертовский выводов. Типовое лямбда-исчисление как исчисление доказуемостных термов для естественных выводов. Изоморфизм Карри-Ховарда естественных выводов и типовых лямбда-термов.

5. Полиномы доказательств, их интерпретация как вычислимых операций над доказательствами из гипотез. Формулы, несущие доказательства. Логика доказательств LP. Лемма о подъёме, конструктивное правило усиления. Свойство интернализуемости выводов в LP.

6. Теорема о реализуемости модальности в S4 полиномами доказательств. Решение задачи Гёделя о реализуемости модальной и интуиционистской логики в классической логике доказательств. Точная математическая форма семантики Брауэра-Гейтинга-Кол­мо­го­рова. Проблема бесконечности знания в эпистемической логике (logical omniscience problem), подход к её решению, основанный на полиномах доказательств.

7. Формализация доказательств с единственным заключением. Аксиома унификации. Функциональная логика доказательств FLP, её модели в ссылочных структурах данных.



8. Свойство интернализуемости доказательств как правило вывода. Рефлексивное лямбда-исчисление как замыкание интуиционистской логики правилом интернализации. Рефлексивная комбинаторная логика. Новые комбинаторы: d (денотат), o (интерпретатор), c (кодировщик), их подразумеваемая семантика. Возможности расширения существующих типовых языков программирования.
скачать файл


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