Применения метода резолюций в алгебре предикатов

1. Применения метода резолюций в алгебре предикатов

2.

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

3.

Пример.
Методом
резолюций
доказать
тождественную
истинность формулы
Условие
Для формулы
равносильно
.
найдем ПНФ и ССФ.

4.

ПНФ формулы
ССФ формулы
Для доказательства невыполнимости этой формулы достаточно
доказать
противоречивость
множества
дизъюнктов
ее
конъюнктивного ядра

5.

Резолютивный вывод формулы 0 из множества дизъюнктов
:
,
где

6.

где

7. Аксиоматический метод

8.

Было определено множество формул алгебры
высказываний FАВ
Затем было выделено подмножество этого
множества TАВ FАВ, состоящие из специальных
формул – тавтологий.
При этом в основе определения тавтологии
лежит понятие интерпретации формул, т.е.
придание
некоторого
конкретного
содержательного смысла входящих в них
переменных. Такой подход к логическим
формулам носит теоретико-множественный
характер и называется семантическим.

9.

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

10.

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

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

12.

Множество
аксиом
Ax(ИВ)
исчисления
высказываний описывается следующими тремя
схемами аксиом:
( A1 ) ,
A2 1 2 3 1 2 1 3 ,
A3 ,
где , , i i 1,2,3 – произвольные формулы
исчисления высказываний.

13.

Исчисление высказываний имеет единственное
правило вывода, которое называется правилом
заключения или правилом modus ponens (сокращенно
MP) и которое для произвольных формул
исчисления высказываний , определяется по
формуле MP , .
Символически это правило вывода записывается
следующей схемой:
,
MP :
.

14.

В основе алгоритма вывода теорем исчисления
высказываний лежит следующее понятие.
Определение. Формула называется теоремой
исчисления высказываний, если найдется такая
конечная последовательность формул 1 ,..., n , в
которой:
1) n = ;
2) каждая формула i 1 i n либо является
аксиомой, либо получается из некоторых двух
предыдущих формул j , k 1 j, k i по
правилу вывода MP.
Последовательность формул 1 ,..., n называется
выводом или доказательством формулы .

15.

Вывод формулы сокращенно обозначают
символом | и говорят, что « есть теорема».
Множество всех таких теорем обозначается
символом Th(ИВ) и называется теорией
исчисления высказываний.
Главной целью построения исчисления
высказываний является определение такой
теории Th(ИВ), которая совпадает с множеством
тавтологий TАВ.

16.

Лемма.
Справедливы следующие утверждения:
1)всякая аксиома ИВ является тавтологией;
2)результат применения правила вывода MP
к любым тавтологиям , дает
тавтологию ;
3)всякая теорема ИВ является тавтологией,
т.е. выполняется Th(ИВ) TАВ.

17.

Теорема полноты ИВ.
Всякая тавтология является теоремой ИВ,
т.е. выполняется TАВ Th(ИВ) и, следовательно,
TАВ=Th(ИВ).

18.

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

19. Исчисление предикатов

20.

Множество аксиом Ax(ИП) исчисления
предикатов описывается пятью схемами аксиом
– тремя определенными в предыдущем разделе
схемами A1 A3 , в которых , , i i 1,2,3
являются
произвольными
формулами
исчисления предикатов, и двумя новыми
схемами:
( A4 ) x ( x) ( y )
для произвольной формулы (x), в которую y
не входит связно;
A5 x ( x) x ( x)
для таких формул , , что x в формулу не
входит свободно.

21.

Исчисление предикатов имеет два правила
вывода – правило modus ponens (сокращенно,
MP) и правило обобщения (сокращенно, Gen),
которые для произвольных формул исчисления
предикатов , символически записываются
следующими схемами:
,
MP :
Gen :
и
x .

22.

Определение. Формула называется теоремой
исчисления предикатов, если найдется такая
последовательность 1 ,..., n , в которой n = и
каждая формула i 1 i n либо является
аксиомой,
либо
получается
из некоторых
предыдущих формул этой последовательности
j 1 j i по одному из правил вывода MP или
Gen. При этом 1 ,..., n называется выводом или
доказательством формулы .
Вывод формулы обозначают | и говорят,
что « есть теорема». Множество всех таких теорем
обозначается символом Th(ИП) и называется
теорией исчисления предикатов.

23.

Цель построения исчисления предикатов определение такой теории Th(ИП), которая
совпадает с множеством тавтологий TАП.
Лемма 1.
Справедливы следующие утверждения:
1)всякая аксиома ИП является тавтологией;
2)результат применения правил вывода MP и
Gen к тавтологиям является тавтологией;
3)любая теорема ИП является тавтологией
ИП, т.е. имеет место включение
Th(ИП) TАП.

24.

Доказательство TАП Th(ИП) было получено
австрийским математиком К.Геделем в 1930
году.
Теорема полноты ИП.
Формула исчисления предикатов в том и
только том случае является тавтологией, если
она есть теорема ИП, т.е. выполняется
равенство TАП=Th(ИП).
Таким образом, ИП является адекватным
инструментом получения логических законов.

25.

Теорема о непротиворечивости ИП.
В исчислении предикатов невозможно
доказать никакую формулу вместе с ее
отрицанием .
С другой стороны, английский математик
А.Черч в 1936 году доказал следующий
принципиально важный результат.
Теорема о неразрешимость ИП.
Не существует универсальной эффективной
процедуры (алгоритма), которая для любой
формулы определяет, является ли эта формула
теоремой ИП.

26. Элементы теории алгоритмов

27.

Важные математические проблемы имеют вид:
для некоторого данного множества X найти
эффективную процедуру (т.е. алгоритм), с помощью
которой можно для каждого элемента x этого
множества X определить за конечное число шагов,
будет этот элемент обладать некоторым данным
свойством P или нет (т.е.
или
).
Решением такой проблемы является построение и
обоснование искомого алгоритма.
Массовые задачи – задачи распознавания и
оптимизации.

28.

Примеры массовых задач:
ВЫП (SАТ) –
задача выполнимости
формулы логики высказываний.
ТЕОРЕМА (THM) – задача доказуемости
формулы логики предикатов.