x |
y |
x«y |
0 |
0 |
1 |
0 |
1 |
0 |
1 |
0 |
0 |
1 |
1 |
1 |
Литералом или литерой называется атом или его отрицание.
Например: p, q, ùl
Рекуррентное определение формул:
- Атом – это формула
- Если F – формула, то ùF – формула
- Если F1, F2 - формулы, то F1ÚF2, F1ÙF2, F1®F2, F1«F2 – формулы.
Интерпретация формулы – это отображение, ставящее в соответствии истинностным значениям атомов истинностное значение формулы.
Например:
Пусть имеется формула:
(p®q)Úl;
пусть p=0, q=0, l=0, следовательно, F=1
p=1, q=0, l=0, следовательно, F=0
Формула, истинная при всех интерпретациях, называется общезначимой. Формула, ложная при всех интерпретациях, называется противоречивой. Формулы f и q являются эквивалентными, если они истинны в одних и тех же интерпретациях.
Множество {0,1} (true, false) c определенными на нем операциями конъюнкции и дизъюнкции образует булеву алгебру:({0,1}, Ú, Ù) – Булева алгебра
Для любых формул F1, F2, F3 справедливы следующие свойства.
- Коммутативность
F1ÙF2ºF2ÙF1.
F1ÚF2ºF2ÚF1..
- Ассоциативность
(F1ÚF2)ÚF3ºF1Ú(F2ÚF3).
(F1ÙF2)ÙF3ºF1Ù(F2ÙF3).
- Дистрибутивность
F1Ù(F2ÚF3)º(F1ÙF2)Ú(F1ÙF3);
F1Ú(F2ÙF3)º(F1ÚF2)Ù(F1ÚF3).
- Законы единицы
FÙ1ºF; FÚ1º1;
- Законы нуля
FÚ0ºF; FÙ0º0;
- Закон исключённого третьего
FÚùFº1.
«закон» противоречия
FÙùFº0.
- Законы поглощения
F1Ù(F1ÚF2)ºF1;
F1Ú(F1ÙF2)ºF1.
- Законы де Моргана
ù(F1ÚF2)ºùF1ÙùF2;
ù(F1ÙF2)ºùF1ÚùF2.
- Правила замены
F1®F2ºùF1ÚF2;
F1«F2=(F1®F2)Ù(F2®F1)º(ùF1ÚF2)Ù(ùF2ÚF1).
- ù ùFºF.
Все приведенные выше законы легко доказываются с помощью таблиц истинности.
2.1.2. Понятие о логическом следствии.
Формула G называется логическим следствием формул F1,…,Fn (F1,…,FnÞG), если она истинна в тех же интерпретациях, где истинны формулы F1,…,Fn.
Имеют место две теоремы дедукции.
- Формула G является логическим следствием формул F1,…,Fn тогда и только тогда, когда формула (F1Ù…ÙFn)®G общезначима, т.е. F1,…,FnÞG Û (F1Ù…ÙFn)®Gº1.
- Формула G является логическим следствием формул F1,…,Fn тогда и только тогда, когда формула (F1Ù…ÙFn)®G противоречива, т.е. F1,…,FnÞG Û (F1Ù… ÙFnÙùGº0).
Говорят, что формула F представлена в конъюнктивной нормальной форме (КНФ), если она имеет вид: F=G1Ù…ÙGn, где "Gi является дизъюнктом (клозом), т.е. имеет вид l1Ú…Úlm, где l1,…,lm – литеры.
Например, (pÚq)Ù(qÚùlÚùf)Ùc.
Говорят, что формула F представлена в дизъюнктивной нормальной форме (ДНФ), если она имеет вид: F=G1Ú…ÚGn, где "Gi является конъюнктом (кьюпом), т.е. имеет вид l1Ù…Ùlm, где l1,…,lm – литеры.
Доказано, что любая формула в логике высказываний может представляться как в КНФ, так и в ДНФ.
Множество клозов G1,…,Gn называется противоречивым, если противоречива их конъюнкция.
Пусть, поставлена задача доказать, что F1,…,Fn ÞG. Если формулы F1,…,Fn и формула ùG представлены в КНФ, то доказательство с использованием второй теоремы дедукции (доказательство противоречивости формулы F1Ù…ÙFnÙùG) сводится к задаче доказательства противоречивости множество клозов. Для этого удобно использовать метод резолюции. Остановимся на нём подробнее.2.1.3. Метод резолюции в ЛВ.
Пусть C1 и C2 – клозы. Клоз C1ÚC2 называется бинарной резольвентой (или просто резольвентой) клозов C1Ú p, C1Úùp.
Например, pÚqÚùl pÚùlÚf
ùqÚf
Литеры p, ùp при этом называются контрарными.
Доказано, что резольвента является логическим следствием.
Замечание.Клоз можно рассматривать как множество литер. Так клоз pÚùlÚf фактически есть множество литер {p,ùl, f}. Таким образом, мы приходим к понятию пустого клоза ( ).
Метод резолюции сводится к последовательному получению резольвент, каждая из которых является логическим следствием. Из данного множества клозов (так называемого входного множества) пытаются вывести пустой клоз. Этот процесс называется резолютивным выводом пустого клоза или опровержением множества клозов.
Например:
Дано: p®q
q® f
Доказать: p®f
Доказательство: 1) Приводим все формулы к КНФ: ùpÚq, ùqÚf
ù( p®f)= ù(ùpÚf)=pÙùf
2) Производим резолюцию:
ùpÚq
ùpÚf
f
ùqÚf
p
ùf
p
ùf
ùf
Имеет место теорема о полноте резолютивного вывода. Множество клозов противоречиво тогда и только тогда, когда из него методом резолюции можно вывести пустой клоз.
Приведем формальный алгоритм, который проверяет, является ли формула G логическим следствием некоторых других формул.
ВХОД: S – входное множество клозов.
ВЫХОД: OK – удается получить пустой клоз, NO – не удается.
M:=S; // - M-текущее множество клозов.
while ÏM do
if not Choose (M, C1, C2, p1, p2) then return(NO);
C:=R(M, C1, C2, p1, p2); // - вычисление резольвенты.
M:=M È {c}; // - пополнение текущего множества.
end
return (OK); //получен пустой клоз
Примечание.
1: Функция R вычисляет резольвенту двух клозов С1 и С2, содержащих контрарные литеры р1 и р2. Результатом работы функции является резольвента.
2. Процедура Choose выбирает в текущем множестве клозов М два резольвируемых клоза, то есть два клоза, которые содержат унифицируемые контрарные литеры. Если таковые есть, то процедура их возвращает, в противном случае возвращается пустое множество. Конкретные реализации процедуры Choose называются стратегиями метода резолюции.
Очевидно, что данный алгоритм может «зависнуть». Например, такое произойдет, если для резолюции постоянно выбирается одна и та же пара клозов. Поэтому стратегия резолюции должна гарантировать конечность алгоритма.
Стратегия, как будет показана ниже, может либо гарантировать получение пустого клоза (полная стратегия) или не гарантировать (неполная стратегия). В соответствии с теоремой о полноте резолютивного вывода полный перебор всевозможных вариантов является полной стратегией.
