Similar presentations:
Тавтологии алгебры предикатов (лекция 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.
Пример. Результатом скулемизации формулыявляется следующая ССФ