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

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

2.

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

3.

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

4.

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

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

6.

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

7.

Одну из основных систем автоматического
поиска доказательства разработали Жак Эрбран,
Дж.Робинсон и др. на основе алгоритма поиска
интерпретации,
опровергающей
рассматриваемую формулу. Так как для
общезначимых
формул
опровергающих
интерпретаций нет, то такой алгоритм
заканчивает работу за конечное число шагов.

8.

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

9.

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

10.

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

11.

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

12.

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

13.

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

14.

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

15.

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

16.

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

17.

Пример. Как показано в
примере, замкнутая формула
предыдущем
y x P( x, y ) y x Q( x, y )
имеет ПНФ
y x z ( P( x, y ) Q( z, y )) ,
результатом скулемизации которой является
формула
x z ( P( x, c) Q( z, c))
с новым предметным символом c.
Формула является ССФ формулы .

18. Метод Эрбрана

19.

Правило 1. Противоречивость замкнутой
формулы исчисления предикатов Φ равносильна
противоречивости ее скулемовской стандартной
формы , которая является универсально
замкнутой формулой
i1 xi1 ... ik xik
с конъюнктивным ядром D1 ... Dm , где
D1 ,..., Dm
– некоторые дизъюнкты литер
исчисления предикатов.
С другой стороны, универсально замкнутая
формула противоречива в том и только том
случае, если она невыполнима.

20.

Так как кванторы общности проносятся через
конъюнкции, то формула представляется в
виде:
i xi ... i xi =
1
1
k
k
= i xi ... i xi D1 ... i xi ... i xi Dm
1
1
k
k
1
1
k
k
и, значит, ее невыполнимость равносильна
невыполнимости множества универсальных
замыканий
D1 i1 xi1 ... ik xik D1 ,..., Dm i1 xi1 ... ik xik Dm
формул
из
S {D1 ,..., Dm } .
множества
дизъюнктов

21.

Невозможно рассмотреть все интерпретации
множества формул S на всех областях
интерпретации, так как множество таких областей
интерпретации бесконечно.
Однако Эрбран показал, что при доказательстве
невыполнимости такого множества формул S
можно
ограничиться
рассмотрением
интерпретаций в одной специальной области
интерпретации,
которая
называется
эрбрановским универсумом.

22.

Пусть C S – множество всех предметных
FS
символов
и
–
множество
всех
функциональных символов, встречающихся в
формулах множества S.
На первом шаге индукции для множества S
определяется множество констант нулевого
уровня H0 по правилу:
H 0 CS , если C S , и H 0 {a} для одного
нового постоянного символа a, если CS .

23.

Затем для каждого натурального значения
i 1,2,... определяется множество констант iго уровня Hi как объединение множества Hi-1 с
множеством всех выражений вида
f (t1 ,...,tn ) ,
где t1,...,tn H j и f – n-арный функциональный
символ из множества FS .
Объединение всех множеств Hi (i 0,1,2, . . .
называется
эрбрановским
универсумом
множества S и обозначается H .

24.

Примеры. 1. Для множества дизъюнктов
S P( x, f ( y )) Q( x, c), P( x, y ) Q( f (c), x)
эрбрановский универсум
H {c, f (c), f ( f (c)), f ( f ( f (c))),...}.
2. Для множества дизъюнктов
S P( x, f ( x, y )) Q( x, c), P( x, f ( y, g ( z ))) Q( g (c), x)
эрбрановский универсум
H {c, f (c, c), g (c), f (c, f (c, c)), f (c, g (c)),..., g ( g (c)),...}

25.

Интерпретации множества формул S в H
называются H-интерпретациями, если:
1) для каждого предметного символа c,
встречающегося в формулах множества S,
выполняется равенство: (c) c ;
2) для каждого n-арного функционального
символа f , встречающегося в формулах
множества S, соответствующая n-арная
операция ( f ) f H на множестве H
удовлетворяет условию: f H (t1 ,...,tn ) f (t1 ,...,tn )
при любых t1 ,...,tn H ;

26.

3) интерпретация (P) каждого
n-арного
предикатного символа P, встречающегося в
формулах множества S, определяется как nарное отношение ( P) PH на множестве
H .
.

27.

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

28.

Вывод. Доказательство противоречивости
формул исчисления предикатов сводится к
доказательству
противоречивости
конечных
множеств дизъюнктов S.
Для этого строится резолютивный вывод 0
из множества дизъюнктов S.