Линейная резолюция. Линейный вывод.

↑

▷ Содержание

⇐ ПредыдущаяСтр 5 из 6Следующая ⇒

Линейная резолюция. Линейный вывод.

Линейным выводом из множества дизъюнктов S называется последовательность дизъюнктов , ,…,

1)  принадлежит S

2) , i=1,2,…,n-1 является резольвентой дизъюнктов  и

3) принадлежит S

4)  является некоторым дизъюнктом , предшествующим в выводе , т.е. j<i.

Упорядоченный дизъюнкт.

Дизъюнкт с упорядоченной последовательностью литер называется упорядоченным дизъюнктом. А V В  В V А

На множестве литер вводится отношение порядка. Литера L с индексом 2 старше , если  следует за  в записи дизъюнкта. P(a) V P(b) V P(c), старшая - P(c), самая младшая P(a).

Упорядоченный фактор дизъюнкт.

Если 2 или больше литер с одинаковыми знаками упорядоченного дизъюнкта С имеют унификатор , то упорядоченный дизъюнкт, полученный из вычеркиванием любой литеры, соответствующей младшей литере, называют упорядоченным фактором-дизъюнктом С.

С = P(х) V R(х) V P(а)

Тогда:  = P(а) V R(а) V P(а) 

Фактор дизъюнкт: P(а) V R(а)

Упорядоченная бинарная резольвента.

Пусть мы имеем 2 упорядоченных дизъюнкта  и , которые содержат  и = ù  соответственно.  и  могут быть унифицированы унификатором . Тогда упорядоченная бинарная резольвента С – упорядоченный дизъюнкт, полученный путем выполнения следующих действий

1) Определение:  и

2) Записи дизъюнкции  и  без изменения порядка их литер:  V  

3) Удаление из выражения:  и

4) Вычеркивание из полученной последовательности любой литеры, которая идентична младшей литере.

Познавательные статьи:



Техника прыжка в длину с разбега

Организация работы процедурного кабинета

Области применения синхронных машин

Оптимизация по Винеру и Калману