Линейная резолюция в L

Определение. Для данного множества S дизъюнктов и дизъюнк­та С₀ из S линейный вывод дизъюнкта С_n из S с верхним дизъюнктом С₀ - это вывод, изображенный на рис. 1, где

1) для i = 0, 1, ..., n-1 дизъюнкт C_i+1 есть резольвента дизъюнкта С_i и В_i; дизъюнкты C_i называется центральными В_i - боковыми.

2) В_i либо принадлежит S, либо есть С_j для некоторого j < i.Показано, что линейная резолюция является полной, т.е. для любого противоречивого множества дизъюнктов всегда выводится пустой дизъюнкт.

Дополнительное усиление рассмотренной стратегии предложено Лавлендом, Ковальским и Кюнером. Ими установлены условия, при ко­торых центральный дизъюнкт позднее может участвовать в роли боко­вого дизъюнкта. Это свойство позволяет сократить число лишних дизъюнктов, поскольку становится ясно, будет или нет тот или иной центральный дизъюнкт использован для порождения пустого дизъюнкта. Прежде всего, множество литер произвольным образом упорядочи­вается, т.е. считается известным, какую литеру поставить левее в записи дизъюнкта, а какую правее. Например, пусть P > Q > R > тогда считаем, что дизъюнкт PÚQÚ записан верно, а PÚ ÚQ- нет.

При порождении резольвент отсекаемая литера включается в пред­ставление резольвенты, но при этом указывается в рамке. Например, если

C₁ = P Ú Q

C₂ = Ú R,

то резольвента С₁ и С₂ имеет вид

P Ú Ú R.

Литеры в рамке служат для учета отрезанных литер: они не участ­вуют в дальнейшем порождении резольвент.

Рассмотрим дизъюнкт специального вида, в котором последняя ли­тера не обрамлена и для этой последней литеры имеется контрарная об­рамленная литера, например, Ú Ú .

Дизъюнкт такого типа называется редуцируемым. Если С - редуци­руемый дизъюнкт, то его можно сократить за счет отбрасывания по­следней литеры, а также всех обрамленных литер, за которыми не следует необрамленной литеры. Для редуцируемого дизъюнкта Ú Ú это сразу дает .

Следующая лемма формализует введенные определения.

Лемма. Если в некотором выводе С является редуцируемым упоря­доченным дизъюнктом, то существует центральный упорядоченный дизъюнкт C_j (j<1), такой, что редукция С_i+1 дизъюнкта C_i является ре­зольвентой С_i и С_j.

Доказательство. Если С_k и С_k+1, два соседних упорядоченных дизъ­юнкта на рис.7.1, то все литеры дизъюнкта С_k содержатся в С_k+1 (об­рамленные литеры учитываются). Действительно, С_k+1 представляется как

Ú(C_k\{I}) Ú (B_k\ ),

где I - отсекаемая литера.

P Ú

P Ú

С учетом доказанной леммы упорядоченный вывод (называемый OL - выводом) определяется следующим образом:

1) Каждый дизъюнкт В_i либо принадлежит S, либо является ранее порожденным центральным дизъюнктом.

2) Если С_i редуцируемый упорядоченный дизъюнкт, то С_i+1 яв­ляется результатом редукции С_i. В противном случае С_i+1 есть резольвента С_i и В_i, причем В_i при­надлежит исходному множеству дизъюнктов и отсекаемая литера в С_i последняя.

3) В вывод не входят тавтологии.

Пример. Построим OL - вывод пустого дизъюнкта из множества дизъюнктов:

C₁ = P Ú Q,

C₂ = R Ú ,

C₃ = R Ú

C₄ = Ú

C₅ = Ú ;

P > Q > R >

1. Находим резольвенту дизъюнктов С₁ и С₂, для которых отсекае­мая литера последняя

2. Находим резольвенту дизъюнктов С₆ и С₄:

С₇ = P Ú Ú Ú

3. Поскольку дизъюнкт С₇ редуцируем, то сразу находим

С₈ = Р

как результат редукции С₇.

4. Находим резольвенту дизъюнктов С₈ и С₃:

5. Находим резольвенту С₉ и С₅:

C₁₀ = Ú Ú

C₁₀ является редуцируемым дизъюнктом. Следовательно, его редук­ция сразу дает

C₁₁ = .

3.5.2.2 Метод линейного вывода в L Лавленда, Ковальского и Кюнера

Рассмотрим пример линейного вывода. Пусть дано

Введем дополнительные определения:

1. Входная резолюция – это применение правила резолюции, в котором одна из посылок – входной дизъюнкт (входная резолюция – это частный случай линейной резолюции).

2. Входным дизъюнктом является каждый член исходного множества S дизъюнктов.

3. Входной вывод – это вывод, в котором любое применение резолюции является входной резолюцией.

4. Входное опровержение – это входной вывод дизъюнкта ÿ из S.

5. Упорядоченный дизъюнкт – это последовательность различных литер. Это означает, что мы должны установить порядок всех литер в дизъюнкте. Примем соглашение, что литера L₂ меньше, чем литера L₁, в дизъюнкте С в точности тогда, когда L₂ следует за L₁ в последовательности, указанной в задании этого дизъюнкта. Таким образом, последняя литера всегда будет считаться наибольшей в дизъюнкте.

Уточним, что же предложили Лавленд, Ковальский и Кюнер.

Для этого рассмотрим пример. Здесь дизъюнкт p не является входным дизъюнктом. При этом легко видеть, что входное опровержение для исходного множества S отсутствует. Поэтому неизбежно использование одного из центральных дизъюнктов в качестве бокового. Однако, тогда возникает необходимость поиска необходимого и достаточного условия, при котором боковой дизъюнкт должен быть одним из ранее порожденных центральных дизъюнктов.

Так вот, информация об отрезаемых литерах, записанная надлежащим образом, а также использование упорядоченного дизъюнкта дают возможность определить это условие. Уточним один важный момент - о записи отрезаемых литер.

Пусть С₁ и С₂ следующие упорядоченные дизъюнкты:

Результатом резолюции этой пары будет упорядоченный дизъюнкт – (p Ú r). При этом литеры q и - контрарны, примем соглашение, что результат их дизъюнкции удалять не будем, а запишем его в виде одной левой литеры, обрамленной ее в рамку. Обрамленная литера – это отрезаемая литера, которая учитывается в дальнейших резолюциях следующим образом:

1. Обрамленную литеру должны выбрасывать только тогда, когда за ней не следует никакая необрамленная литера.

2. Если в упорядоченном дизъюнкте имеется более одного вхождение одной и той же необрамленной литеры, то всегда сохраняем самое левое вхождение, остальные совпадающие отбрасываем. Этот процесс называется отождествлением влево.