- •1.Алгебра высказываний; пропозициональные связки и формы, истинностные таблицы
- •2.Алгебра высказываний; тавтологии и противоречия
- •3.Алгебра высказываний; логическая эквивалентность и логическое следствие
- •4. Алгебра высказываний; дизъюнктивная и конъюнктивная нормальные формы
- •5. Алгебра высказываний; полные системы функций, базис
- •6. Понятие формальной аксиоматической теории. (фат)
- •7. Исчисление высказываний, как формальная аксиоматическая теория (фат).
- •8. Формальная аксиоматическая теория (фат), определение аксиомы, правило вывода
- •9. Формальная аксиоматическая теория (фат), формализация понятий теоремы и ее док-ва.
- •10. Формальная аксиоматическая теория (фат),теорема дедукции, правило силлогизма и перестановки посылок.
- •11.Исчисление высказываний: связь между теоремами исчисления высказываний и тавтологиями.
- •12. Логика предикатов: понятия терма и предиката, кванторы.
- •13. Логика предикатов: логическая общезначимость.
- •14. Логика предикатов: эквивалентность формул логики предикатов.
- •15. Логика предикатов: нормальные.
- •16 Теория алгоритмов. Нормальные алгорифмы Маркова.
- •17.Теория алгоритмов. Интуитивное понятие алгоритма.
- •18.Теория алгоритмов. Нормальные алгорифмы Маркова,как уточнение понятия алгоритма.
- •19. Теория алгоритмов. Машина Поста.
- •20 Теория алгоритмов. Машина Тьюринга.
- •21. Исчисление высказываний. Построение доказательства Методом Modus ponens
- •22. Исчисление высказываний. Построение доказательства методом резолюций
- •23. Исчисление высказываний. Построение доказательства методом Вонга
- •X, l X; r,
- •X y, (X → y) u, z → (y → w) (w → X) → (z X).
- •X y, X y u,zy w w X;z; X.
- •24. Исчисление высказываний. Перенос высказываний через знак выводимости
21. Исчисление высказываний. Построение доказательства Методом Modus ponens
Одним из возможных вариантов (Гильбертовской) аксиоматизации логики высказываний является следующая система аксиом:
;
;
;
;
;
;
;
;
;
;
.
вместе с единственным правилом:
Modus ponens(правило заключений): если A и A→B — выводимые формулы, то B также выводима.
Форма записи: , гдеA, B— любые формулы.
Принцип работы правил вывода хорошо иллюстрирует следующий пример:
«Если известно, что высказывание «А» влечет (имплицирует) высказывание «В», а также известно, что высказывание «А» истинно, то, следовательно, «В» истинно»
22. Исчисление высказываний. Построение доказательства методом резолюций
В математической логике и автоматическом доказательстве теорем, правило резолюций – это правило вывода, восходящее к методу доказательства теорем через поиск противоречий; используется в логике высказываний и логике предикатов первого порядка. Правило резолюций, применяемое последовательно для списка резольвент, позволяет ответить на вопрос, существует ли в исходном множестве логических выражений противоречие. Правило разработано Джоном Аланом Робинсоном в 1965.Пусть C1 и C2 - два предложения в исчислении высказываний, и пусть , а , где P - пропозициональная переменная, а C'1 и C'2 - любые предложения (в частности, может быть, пустые или состоящие только из одного литерала).
Правило вывода называется правилом резолюции.
Предложения C1 и C2 называются резольвируемыми (или родительскими), предложение - резольвентой, а формулы P и - контрарными литералами.
23. Исчисление высказываний. Построение доказательства методом Вонга
Близким к методу резолюций является метод Вонга, в котором тоже используется сконструированная конъюнктивно-дизъюнктивная нормальная форма представления исходной клаузы, а аксиому порядка заменяет клауза Вонга:
X, l X; r,
здесь X пробегает некоторые буквы, входящие в клаузу, а L и R — определенные комбинации дизъюнктов и конъюнктов.
Конструктивнаяпроцедура доказательства сводится к последовательной разбивке дизъюнктов или конъюнктов таким образом, чтобы слева и справа от метаимпликации появилась одна и та же буква X. Если в результате такой разбивки все конечные клаузы приобретают вид клаузы Вонга, то и исходная клауза была составлена верно. Разберем метод Вонга на примере доказательства справедливостиправила отделения:
А, А → В В или А, А В В.
Здесь имеется только один дизъюнкт, который можно разбить на две новых клаузы:
А, А В и А, В В.
Вторая клауза удовлетворяет и аксиоме порядка и клаузе Вонга. В качестве Х в ней выступает терм В, L = А и R = 0. Первая же клауза тоже будет удовлетворять необходимым требованиям, но только после того, как терм Аиз левой части клаузы с противоположным знаком перенести в правую часть. Тогда будем иметь:
А А; В где Х = А, L = 1 и R = В.
При большом числе термов в исходной клаузе прибегают к специальной нумерации производных клауз, чтобы не запутаться. Пусть требуется установить справедливость следующей клаузы: