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

Пусть 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

Дата добавления: 2015-09-06