2.1.2. Понятие о логическом следствии.

Формула G называется логическим следствием формул F₁,…,F_n (F₁,…,F_nG), если она истинна в тех же интерпретациях, где истинны формулы F₁,…,F_n.

Имеют место две теоремы дедукции.

1. Формула G является логическим следствием формул F₁,…,F_n тогда и только тогда, когда формула (F₁…F_n)G общезначима, т.е. F₁,…,F_nG  (F₁…F_n)G1.

2. Формула G является логическим следствием формул F₁,…,F_n тогда и только тогда, когда формула (F₁…F_n)G противоречива, т.е. F₁,…,F_nG  (F₁_… F_nG0).

Говорят, что формула F представлена в конъюнктивной нормальной форме (КНФ), если она имеет вид: F=G₁…G_n, где G_i является дизъюнктом (клозом), т.е. имеет вид l₁…l_m, где l₁,…,l_m – литеры.

Например, (pq)(qlf)c.

Говорят, что формула F представлена в дизъюнктивной нормальной форме (ДНФ), если она имеет вид: F=G₁…G_n, где G_i является конъюнктом (кьюпом), т.е. имеет вид l₁…l_m, где l₁,…,l_m – литеры.

Доказано, что любая формула в логике высказываний может представляться как в КНФ, так и в ДНФ.

Множество клозов G₁,…,G_n называется противоречивым, если противоречива их конъюнкция.

Пусть, поставлена задача доказать, что F₁,…,F_n G. Если формулы F₁,…,F_n и формула G представлены в КНФ, то доказательство с использованием второй теоремы дедукции (доказательство противоречивости формулы F₁…F_nG) сводится к задаче доказательства противоречивости множество клозов. Для этого удобно использовать метод резолюции. Остановимся на нём подробнее.

2.1.3. Метод резолюции в лв.

Пусть C₁ и C₂ – клозы. Клоз C₁C₂ называется бинарной резольвентой (или просто резольвентой) клозов C₁ p, C₁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, C₁, C₂, p₁, p₂) then return(NO);

C:=R(M, C₁, C₂, p₁, p₂); // - вычисление резольвенты.

M:=M  {c}; // - пополнение текущего множества.

end

return (OK); //получен пустой клоз

Примечание.

1: Функция R вычисляет резольвенту двух клозов С₁ и С₂, содержащих контрарные литеры р₁ и р₂. Результатом работы функции является резольвента.

2. Процедура Choose выбирает в текущем множестве клозов М два резольвируемых клоза, то есть два клоза, которые содержат унифицируемые контрарные литеры. Если таковые есть, то процедура их возвращает, в противном случае возвращается пустое множество. Конкретные реализации процедуры Choose называются стратегиями метода резолюции.

Очевидно, что данный алгоритм может «зависнуть». Например, такое произойдет, если для резолюции постоянно выбирается одна и та же пара клозов. Поэтому стратегия резолюции должна гарантировать конечность алгоритма.

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