Тавтологии алгебры предикатов (лекция 6)

1.

Тавтологии алгебры
предикатов

2.

С другой стороны, в алгебре предикатов можно
получить много принципиально новых тавтологий с
помощью следующих свойств кванторов.
Лемма 2. Для любых формул , следующие
формулы являются тавтологиями:
1. x x , x x ,
x x , x x ;
2. x y y x , x y y x ;
3. x ( ) x x ,
x ( ) x x ;

3.

4. x ( ) x , где – символ одной
из операций , ;
5. x ( ) x , где – символ одной из
операций , ,
если в формулу предметная переменная x не
входит свободно; а также
6. x ( ) ( x ) ,
x ( ) ( x ) ,
7. x ( ) ( x ) ,
x ( ) ( x ) .

4.

Логическая равносильность
формул алгебры предикатов

5.

Определение. Формулы алгебры предикатов
, называется логически равносильными, если
результат применения к ним логической
операции эквивалентность является
тавтологией.
В этом случае записывают , или просто
.
Таким образом, означает, что | .

6.

Теорема 1 (Взаимосвязь между кванторами).
Для любой формулы справедливо равенство:
x y y x , x y y x .
С другой стороны, если в формулу
предметные переменные x,y входят свободно,
то равенство
y x x y
не выполняется, так как в этом случае формула
y x x y
не является тавтологией.

7.

Теорема 2. Пусть формула (x) не содержит
предметную переменную y и формула ( y )
получается из (x) заменой всех свободных
вхождений переменной x на предметную
переменную y.
Тогда формулы x (x) и x (x) будут
логически
равносильны
соответственно
формулам y ( y ) и y ( y) , т.е. выполняются
равенства:
x ( x) y ( y) и x ( x) y ( y) .

8.

Теорема 3 (Законы де Моргана для кванторов). Для
любой
формулы
справедливы
следующие
утверждения:
x x , x x ,
x x , x x .
Теорема 4 (Взаимосвязь кванторов с конъюнкцией и
дизъюнкцией). Для любых формул , справедливы
следующие утверждения:
x ( ) x x ,
x ( ) x x .
Если в формулу предметная переменная x не входит
свободно, то справедливы также утверждения:
x x , x x , где
– символ одной из операций , .

9.

Теорема
6
(Взаимосвязь
кванторов
с
импликацией). Если в формулу предметная
переменная x не входит свободно, то для любой
формулы справедливы следующие утверждения:
x ( ) x , x ( ) x .
Если же предметная переменная x не входит
свободно в формулу , то для любой формулы
справедливы утверждения:
x ( ) x , x ( ) x .

10.

Следствие
7.
Любая
формула
представляется в следующем виде:
K1 x1 ... K n xn ,
где K1 ,..., K n – некоторые кванторы и –
формула без кванторов.
Таким образом, каждая формула логически
равносильна формуле K1 x1 ... K n xn , в которой
все кванторы стоят в самом начале формулы и
которая называется предваренной нормальной
формой (сокращенно ПНФ) формулы .

11.

Алгоритм приведения формулы к ПНФ:
1) преобразуем формулу в эквивалентную ей
формулу , которая не содержит импликации и
эквивалентности и в которой отрицание
действует только на элементарные формулы;
2) в все кванторы последовательно выносим
вперед по теореме 5, при этом кванторы
общности x выносятся из конъюнкции и
кванторы существования x выносятся из
дизъюнкции, а для выноса кванторов общности
x из дизъюнкции и кванторов существования
x из конъюнкции переименовываем связанные
переменные x в новые переменные y, которые не
входят в рассматриваемую формулу.

12.

Логическое следование
формул алгебры предикатов

13.

С помощью логического следования формул
определяются общие способы доказательства
взаимосвязи между истинностными значениями
утверждений
посредством
исследования
формальной структуры этих утверждений.
Определение. Формула алгебры предикатов
называется логическим следствием формулы ,
если | , т.е. в любой интерпретации M
формула выполняется при любой оценке
, при которой
предметных переменных
выполняется формула .

14.

Определение.
Формула
называется
логическим следствием множества формул ,
если в любой интерпретации M формула
выполняется при любой оценке предметных
переменных , при которой выполняются все
формулы из .
Такое логическое следствие
обозначается
| и называется логическим следованием.
При этом формулы из называются посылками
и формула – следствием логического
следования | .
В случае, когда { 1 ,..., m } записывают
1 ,..., m | .

15.

Определение. Множество формул называется
противоречивым, если из него логически следует
любая (в том числе и тождественно ложная)
формула . Символически это записывается | .
Лемма 1 (Критерии логического следования).
Условие 1,..., m |
равносильно каждому из
следующих условий:
1 ... m | ,
a)
b) | 1 ... m ,
1 , , m , | .
c)
| .
В частности, | равносильно
Отсюда также следует, что равносильно
тому, что | и | .

16.

Основные правила логического следования:
1) правило отделения (или правило модус поненс –
от латинского modus ponens)
, | ;
2) правило модус толленс (от латинского modus
tollens)
, | ;
3) правило контрапозиции
| ;
4) правило цепного заключения
1 2 , 2 3 | 1 3 .

17.

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

18.

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

19.

Пример.
Формула
общезначима
интерпретации,
интерпретации
PM ( x, y ) x y .
в
но
любой
конечной
не выполнима в
M N
с отношением

20.

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

21.

Автоматическое
доказательство теорем

22.

Существуют алгоритмы поиска доказательства,
которые
для
общезначимых
формул
подтверждают, что эти формулы общезначимы, и
для необщезначимых формул в общем случае не
заканчивают свою работу.
Автоматические
системы
построения
доказательств называют пруверами и предъявляют
им следующие требования:
1) корректность,
2) полнота,
3) эффективность.
Примером такого алгоритма является метод
резолюций.

23.

Метод резолюций
в алгебре предикатов

24.

Первым шагом алгоритма Эрбрана является
приведение
рассматриваемой
формулы
к
специальным нормальным формам, которые
аналогичны ДНФ и КНФ для формул алгебры
высказываний (сокращенно, АВ).

25.

Формула исчисления предикатов Φ находится
в предваренной или пренексной нормальной
форме (сокращенно ПНФ), если она имеет вид
K1 x1 ... K n xn ,
где K1 ,..., K n – некоторые кванторы и –
бескванторная формула, находящаяся в КНФ.
При этом последовательность кванторов
K1 x1 ... K n xn называется кванторной приставкой
и формула называется конъюнктивным
ядром формулы Φ.

26.

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

27.

Элиминация кванторов существования
Пусть
замкнутая
формула
предикатов Φ находится в ПНФ:
исчисления
K1 x1 ... K n xn ,
где
– некоторые кванторы и
( x1 ,..., xn ) – конъюнктивное ядро формулы
Φ, т.е. бескванторная формула со свободными
переменными x1 ,..., xn , находящаяся в КНФ.
K1 ,..., K n

28.

В кванторной приставке формуле Φ можно
удалить любой квантор существования x s для
1 s n по следующему правилу:
1) если левее квантора существования x s в
формуле
Φ не стоит никакой квантор
общности, то выбираем новый предметный
символ c, заменяем этим символом c все
вхождения переменной xs в конъюнктивное
ядро формулы Φ и вычеркиваем x s из
кванторной приставки формулы Φ;

29.

2) если же левее квантора существования x s
стоят кванторы общности
xs ,..., xs
1
m
для значений 1 s1 ... sm s , то выбираем
новый m-арный функциональный символ f,
заменяем все вхождения переменной xs в
конъюнктивное ядро формулы Φ выражением
f ( xs ,..., xs ) и вычеркиваем x s из кванторной
приставки формулы Φ.
1
m

30.

В результате такой замены всех кванторов
существования в формуле Φ получим
замкнутую ПНФ , кванторная приставка
которой получается из кванторной приставки
формулы Φ удалением всех кванторов
существования и которая содержит новые
символы – функциональные или предметные.
При этом формула Φ выполнима или
противоречива одновременно с формулой .

31.

Рассмотренный прием удаления квантора
существования был введен Скулемом и
называется скулемизацией формул. Вводимые в
процессе
скулемизации
новые
функциональные и предметные символы
называются
функторами
Скулема
или
скулемовскими функциями.
Полученную в результате скулемизации
замкнутую ПНФ называют скулемовской
стандартной формой (сокращенно ССФ).

32.

Теорема 2. Любая замкнутая формула
исчисления предикатов
эффективно
преобразуется (с помощью определенного
алгоритма) в логически эквивалентную ей
скулемовскую стандартную форму , которая
называется скулемовской стандартной формой
(сокращенно, ССФ) формулы Φ.
При этом формула Φ выполнима
противоречива одновременно с ее ССФ.
или

33.

Пример. Результатом скулемизации формулы
является следующая ССФ