Сводка определений и основных фактов, страница 4

Определение. Резолютивный вывод для системы дизъюнктов S – это такая конечная последовательность дизъюнктов , что для любого номера i>1 выполняется одно из трех требований:

1) - вариант D из S, т.е. получен из D путем переименования переменных без отождествления;

2) - резольвента двух дизъюнктов с меньшими номерами;

3) - склейка дизъюнкта с меньшим номером

Резолютивный вывод называется успешным (резолютивным опровержением), если его последний дизъюнкт - пустой.

Лемма (о резолюции): Если - резольвента дизъюнктов D и D', то он является их логическим следствием.

Лемма (о склейке): Если - склейка дизъюнкта D, то он является его логическим следствием.

Теорема (корректности резолютивного вывода): Если - резолютивный вывод из семейства дизъюнктов S, то - логическое следствие S.

Лемма (о подъеме для резолюции): Пусть и - основные примеры дизъюнктов и соответственно, а - резольвента и . Тогда дизъюнкт , являющийся резольвентой и , таков, что - основной пример .

Т

е

о

р

е

м

а

(

п

о

л

н

о

т

ы

д

л

я

р

е

з

о

л

ю

ц

и

й

):

Е

с

л

и

S

–

п

р

о

т

и

в

о

р

е

ч

и

в

а

я

с

и

с

т

е

м

а

д

и

з

ъ

ю

н

к

т

о

в

,

т

о

с

у

щ

е

с

т

в

у

е

т

р

е

з

о

л

ю

т

и

в

н

о

е

о

п

р

о

в

е

р

ж

е

н

и

е

S

.

3. Логическое программирование

Логическая программа – это совокупность формул, причем программа позволяет доказать или опровергнуть общезначимость формул, которые в нее входят.

Определение. Хорновским дизъюнктом называется дизъюнкт, в который входит не более одной литеры без отрицания.

Определение. Хорновская логическая программа – множество хорновских дизъюнктов.

Определение. Запрос к программе – задача поиска всех правильных ответов в программе.

Определение. Ответом на запрос с целевыми переменными

называется всякая подстановка

Определение. Ответ

на запрос к логической программе Р называется правильным, если результат подстановки

является логическим следствием Р.

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

Утверждение. I – модель для логической программы Р тогда и только тогда, когда для любого основного примера , если любое

принадлежит I, то и также принадлежит I.

Лемма (о пересечении моделей): Пусть Р – хорновская логическая программа, а М' и М'' - ее модели. Тогда эрбрановская интерпретация М, являющаяся пересечением М' и М'' также будет моделью для Р.

Следствие 1: пересечение произвольного числа моделей для Р также будет моделью.

Следствие 2: пересечение всех моделей для Р также будет ее моделью. Такая модель будет называться наименьшей Н-моделью (ННМ) и обозначаться как

Теорема: Пусть Р – хорновская логическая программа, С - основной терм. С является следствием Р тогда и только тогда, когда он принадлежит ННМ Р.

Определение. Пусть Р – хорновская логическая программа,

- некоторое ее программное утверждение, - запрос, а пересечение формальных параметров (

) с фактическими () пусто. Пусть - подцель запроса G, а

. Тогда запрос

, полученный из G заменой на и последующей унификацией, называется SLD-резольвентой запроса G и программного утверждения D с НОУ

. При этом называется выделенной подцелью, а D – активизированным программным утверждением.

О

п

р

е

д

е

л

е

н

и

е

.

SLD-

р

е

з

о

л

ю

т

и

в

н

ы

м

в

ы

ч

и

с

л

е

н

и

е

м

з

а

п

р

о

с

а

G

к

х

о

р

н

о

в

с

к

о

й

л

о

г

и

ч

е

с

к

о

й

п

р

о

г

р

а

м

м

е

Р

н

а

з

ы

в

а

е

т

с

я

п

о

с

л

е

д

о

в

а

т

е

л

ь

н

о

с

т

ь

п

а

р

, конечная или бесконечная, такая, что

1)

2) Запрос - SLD-резольвента запроса и варианта D' программного утверждения D, такого , а

- НОУ для этой резольвенты.

3) Возможно три варианта вычисления:

А)

- успешное вычисление (SLD-резолютивное опровержение)

Б) бесконечная последовательность – бесконечное вычисление

В) обнаруживается, что очередную SLD-резольвенту построить нельзя – тупиковое вычисление.

Определение. Пусть

- успешное завершение запроса G к хорновской логической программе Р. Тогда подстановка

называется вычислимым ответом на запрос G к логической программе Р.

Определение. Пусть Р – хорновская логическая программа. Тогда множеством успехов Р будет называться следующее множество

- это множество всех атомарных запросов, имеющих успешное SLD-резолютивное вычисление (

- эрбрановскому базису Р).

Определение. Пусть - множество всех подмножеств

(множество всех эрбрановских интерпретаций). Оператором непосредственного следования для логической программы Р называется функция

, такая, что для любого подмножества

(обозначим его I)

, где А_i принадлежит I – т.е. все то, что следует из интерпретации I по правилам логической программы Р.

Утверждение. Для оператора непосредственного следования выполняются свойства:

Определение. Интерпретация I называется неподвижной точкой оператора непосредственного следования, если выполняется равенство

. Множество всех неподвижных точек оператора непосредственного следования обозначим как

Определение.

называется наименьшей неподвижной точкой оператора

, если выполняются 2 свойства:

1)

- неподвижная точка оператора

;

2) для любой другой неподвижной точки I выполняется свойство

.

Наименьшая неподвижная точка обозначается как

.

Теорема

(

о

неподвижных

точках

).

В

хорновской

логической

программе

Р

всегда

существует

наименьшая

неподвижная

точка

,

и

(

т

.

е

.

наименьшая

н

е

п

о

д

в

и

ж

н

а

я

точка

равна

объединению

всех

следствий

конечной

кратности

и

является

наименьшей

эрбрановской

моделью

для

логической

программы

Р

).

Теорема (корректности операционной семантики): Пусть Р – хорновская логическая программа, G – запрос к ней,

- вычисленный ответ на запрос G к Р. Тогда вычисленный ответ

- это правильный ответ.

Следствие.

(т.е. множество успехов является подмножеством наименьшей эрбрановской модели).

Определение. Пусть Р – хорновская логическая программа, - запрос к Р. Тогда квази-SLD-резолютивным вычислением запроса к Р называется последовательность пар

, которая удовлетворяет требованию: если ,

и '

- произвольный унификатор и , то

.

Заметим, что SLD-резолютивное вычисление – частный случай квази-SLD-резолютивного вычисления, поэтому корректность квази-SLD-резолютивного вычисления представляет собой отдельную теорему.

Теорема (о квази-SLD-резолютивных вычислениях): Если атом С входит в наименьшую эрбрановскую интерпретацию (

), то запрос имеет успешное квази-SLD-резолютивное вычисление.

Следствие. Если , то запрос имеет успешное квази-SLD-резолютивное вычисление.

Лемма (о подъеме для SLD-резолюций): Пусть G – запрос к хорновской логической программе Р,

- конечная подстановка, а запрос G

имеет успешное квази-SLD-резолютивное вычисление

. Тогда запрос G имеет успешное SLD-резолютивное вычисление

, причем существует такая конечная подстановка

, что

. Иначе говоря, результат частного случая запроса для квази-SLD-резолютивного вычисления – это результат частного случая запроса для SLD-резолютивного вычисления.

Теорема (о полноте; ван Эмдена): Если атом

, то

.

Теорема (о полноте; Кларка): Пусть G – запрос к хорновской логической программе Р,

- правильный ответ на G. Тогда существует вычисленный ответ

, такой, что для некоторой конечной подстановки