4. Закон контрпозиции

5. Все соотношения (тождества) алгебры логики суть тавтологии и поэтому являются логическими законами.

6. Закон исключения третьего .

7. Закон дистрибутивности и .

8. Закон «гибельная дилемма»

Теорема 1.

Любая формула, которая является тавтологией, может быть приведена к виду и объявлена логическим законом.

Например, – есть тавтология, т.к. обозначив

.

Для представления F в форме введём

.

Исчисление высказываний

Наибольший интерес представляет построение формальной системы, которая среди всех возможных ППФ высказываний выделяет такие, которые являются логическими законами (правильно построенными рассуждениями, логическими умозаключениями, тавтологиями, общезначимыми высказываниями).

Определение 1. Формальная система, порождающая высказывания, которые являются тавтологиями и только их, называются исчислением высказываний (ИВ). Выше было показано, что любая формула высказываний (в том числе и тавтология) может быть приведена к структуре рассуждения (умозаключения), «если Р, то S».

Общезначимые

высказывания

(тавтологии)

Формулы в ИВ считаются выводимыми из аксиом. В каждом выводе из тавтологий выводятся тавтологии. Обозначение: ⊦ ; интерпретация: из выводимо .

Формальная система ИВ определяется:

Формулы – аксиомы являются тавтологиями. Правила вывода в виде также являются тавтологиями.

На сегодняшнее время известно 20 ИВ, которые отличаются друг от друга аксиомами (схемами аксиом) и правилами выводов. Все ИВ обладают 1) свойством полноты – (в них выводимы все тавтологии и только они) 2) набор аксиом обладает минимальной полнотой ( т.е. удаление хотя бы одной аксиомы из набора делает ИВ неполной).

Пример 1. ИВ Уйтхеда и Рассела (19201930, Англия).

Аксиомы

А1. (А  А)  А – закон тавтологии

А2. А  (В  А) – закон добавления

А3. (А  В)(В  А) – закон перестановки

А4. (А  В)((С  А)  (С  В)) – закон суммирования

Правила вывода Р1: Подстановка А вместо В; Р2: Замена на эквивалентную формулу Р3: Modus ponens ⊦ В.

Пример 2. ИВ Никоды (1952, США)

Единственная аксиома с операцией штрих Шеффера:

;

единственное ПВ: ⊦ С.

Методы и алгоритмы проверки выводимости

Определение 2. Пусть задана совокупность ППФ , которая называется посылками (иногда гипотезами), и ППФ – . « » называется логическим следствием . или выводимой из А (записывается как ⊦ ), если является тавтологией (тождественно истинным высказыванием).

Таким образом, задача проверки выводимости сводится к проверке на тождественную истинность. Существует несколько десятков методов и алгоритмов установления тождественной истинности логической формулы.

1. Алгоритм истинностных таблиц (АИТ) для F=AB.

АИТ сводится к последовательной подстановке всех возможных интерпретаций (наборов «истина» и «ложь») переменных, входящих в . Алгоритм останавливается, если значение ложь ( не выполнима, а значит не выводима из на всех интерпретациях); истина ( выполнима на всех интерпретациях, значит суть тавтология и А⊦ . Такой алгоритм требует в наихудшем случае 2ⁿ подстановок (2ⁿ возможных интерпретаций), где «n» число переменных, входящих в формулу F.

2. Алгоритм Квайна (Квайн. 1960 г. США)

Идея: при последовательных подстановках значений переменных можно уменьшить длину формулы, исходя из совокупности проведённых проверок истинности F, и тем самым сокращать число переменных для проверки.

Вводится понятие дерева испытаний, которое по сути дела представляет собой граф всех интерпретаций проверяемой формулы . Квайн назвал его «семантическим деревом».

0

Пример 3. Построение семантического дерева.

Пусть необходимо проверить общезначимость формулы

Семантическое дерево. Каждое левое ребро дерева соответствует переменным , а каждое правое ребро – .

Каждая ветвь (например, самая левая) соответствует набору (pqr), самая правая . Дерево перечисляет все возможные элементарные конъюнкции.

1. 0

   Положим для F (вершина ) , тогда

(напомним, что –

(формула в вершине «1»)

2. Положим для , тогда

.

(формула в вершине «2»)

3

3. 2

   Спустимся до вершины . Положим для , тогда значение (формула в вершине «3»).

4. Поднимемся к вершине , в положим , тогда (формула в вершине «4»).

1

Поднимемся к вершине и в положим , следуя нумерации вершин, находим, что . . Можно заметить характерное правило обхода вершин.

Такой алгоритм обхода вершин семантического дерева называется алгоритмом с возвратом (back tracking). На рисунке показан путь обхода семантического дерева. В процессе обхода вычисляется значение формулы F. Оказывается, что на всех наборах значений . Таким образом F является тавтологией.

3. Метод резолюций (Д.Робинсон, 1965 г., США).

В исчислении высказываний не существует общего, по-настоящему эффективного критерия для проверки выполнимости КНФ, однако есть удобный метод для выявления невыполнимости множества дизъюнктов.

Множество дизъюнктов S не выполнимо тогда и только тогда, когда логическое следствие из него есть пустой дизъюнкт, т. е. дизъюнкт, всегда принимающий значение F. Таким образом, невыполнимость множества дизъюнктов S можно проверить, порождая логические следствия из него до тех пор, пока не получится пустой дизъюнкт.

Алгоритмы доказательства выводимости А⊦B, построенные на основе этого метода, применяются во многих системах искусственного интеллекта, а также являются фундаментом, на котором построен язык логического программирования «Пролог».

Метод резолюций использует несколько принципов.