Курсовая Елфимов МЛ. Курсовой проект по дисциплине Математическая логика и теория алгоритмов Тема Практические задачи математической логики и теории алгоритмов
![]()
|
3 Логический вывод в исчислении высказываний3.1 Метод прямого преобразованияВысказывание B есть логическое следствие высказываний ![]() ![]() ![]() ![]() ![]() Теорема 1. ![]() ![]() ![]() ![]() Теорема 2. Если импликация ![]() ![]() 3.2 Метод семантических таблиц Методы доказательства – это алгоритмические процедуры, посредством которых можно установить, является ли данное высказывание тавтологией. Основой для построения семантических таблиц является атомарная семантическая таблица, [3] которая строится на основе законов исчисления высказываний Пусть ![]() ![]() ![]() ![]() ![]() ![]() ![]() Таблица 4 – Атомарная семантическая таблица
Вершинами семантической таблицы называются все помеченные формулы, встречающиеся в таблице. Вершина семантической таблицы называется особой, если она встречается как корень некоторой атомарной семантической таблицы. В противном случае вершина называется обычной. Ветвь семантической таблицы называется противоречивой, если для некоторого высказывания помеченные формулы tσ и fσ являются вершинами этой ветви. Семантическая таблица называется замкнутой, если каждая непротиворечивая ее ветвь не содержит обычных вершин. В противном случае семантическая таблица называется незамкнутой. Семантическая таблица противоречива, если каждая ее ветвь противоречива. Доказательством или выводом по Бету высказывания ![]() ![]() ![]() ![]() Итак, если замкнутая семантическая таблица с ![]() ![]() ![]() Если не все ветви семантической таблицы противоречивы, то это свидетельствует о том, при некоторой комбинации значений атомов, входящих в исходное выражение, это выражение будет истинным, а при другой комбинации - ложным, то есть, выражение не является тавтологией. |