Лекция 8_3гр.ppsx

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

2.

Любая тавтология алгебры высказываний
является тавтологией алгебры предикатов.
Более того, тавтологии алгебры высказываний
дают возможность легко получать тавтологии
алгебры предикатов с помощью следующего
очевидного результата.
X
– тавтология
,...,
X
Лемма 1. Если
1
n
алгебры высказываний, то для любых формул
,...,
,...,
алгебры предикатов
1
n формула
1
n
является тавтологией алгебры предикатов.

3.

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

4.

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

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

6.

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

7.

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

8.

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

9.

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

10.

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

11.

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

12.

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

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

14.

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

15.

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

16.

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

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

18.

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

19.

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

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

21.

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

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

23.

24.

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

25.

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

26.

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

27.

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

28.

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

29.

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

30.

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

31.

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

32.

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