Принцип резолюций

 

Понятие логической программы рассматривается в контексте с понятием логического вывода.

Из совокупности логических предложений, представляющих знание о задаче, выводится новое утверждение. Для придания операционного характера логическим программам вводится понятие процедурной интерпретации.

Толкование термина «логическая программа» основано на интерпретации правила

P(t1,…,tn) :- P1(a11,…,am1), …, Pk(am1,…,amk)

как процедуры, сводящей решение задачи Р к решению подзадач Р1, …, Рk.

Вопрос рассматривается как вызов процедуры – предикатный символ.

Аргументы предиката вопроса – это фактические параметры.

Аргументы предиката правила Р – это формальные параметры.

Вызов всей программы к исполнению основан на предположении, что некоторая конъюнкция целей является логическим следствием программы.

 

Определение. Значением логической программы (ЗЛП) называется множество выводимых из программы фактов, не содержащих переменных.

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

Простейший случай правила – это

- Программа, не содержащая переменных.

- Вопрос, не содержащий переменных.

Условимся различать программу и задачу. Программа содержит гипотезы: правила-аксиомы и факты. Задача – это вопрос.

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

Цель вывода – доказать, что из множества предложений S можно вывести новое предложение: S |= s.

Будем применять резолюцию к 3 типам предложений:

- Отрицанию Ø(A1, …, An).

- Факту А.

- Конъюнкции (правилу) А ¬ В1, …, Вm.

Для удобства вывода каждое предложение будем метить, например, Si – метка i-го предложения.

Введем резолюцию следующим образом.

S1: Ø( A1, …, Ak-1, Ak, Ak+1,…, An).

S2: Аk ¬ В1, …, Вm.

---------------------------------------------------

S: Ø( A1, …, Ak-1, В1, …, Вm, Ak+1,…, An),

где S1, S2 – родительские правила, S – резольвента.

 

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

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

 

Частный случай:

S1: Ø( A1, …, Ak-1, Ak, Ak+1,…, An).

S2: Аk.

------------------------------------------------

S: Ø( A1, …, Ak-1, Ak+1,…, An).

Простейшие случаи резолютивного вывода:

 

а) S1: Ø A.

S2: А ¬ В.

---------------------------

S: Ø В.

 

б) S1: Ø A.

S2: А.

---------------------------

S: ð. (пустое отрицание, противоречие)

 

Пример. Построить последовательность резольвент для решения задачи: Получает ли Сидоров стипендию?

S1: студент(петров).

S2: студент(сидоров).

S3: сессия-сдана(петров).

S4: сессия-сдана(сидоров).

S5: получает-стипендию(X) :- студент(Х), сессия-сдана(Х).

Допустим, что подается на вход системы

G: получает-стипендию(сидоров)?

 

Решение.

Система вывода преобразует задачу в предложение:

ØG(S0): Øполучает-стипендию(сидоров).

Теперь система ищет предикат получает-стипендию, выбирает предложение S5,

при этом Х примет значение {X:=сидоров}:

S5: получает-стипендию(сидоров) :- студент(сидоров), сессия-сдана(сидоров).

 

Получение первой резольвенты:

L1: Ø (студент(сидоров), сессия-сдана(сидоров)).

S2: студент(сидоров).

------------------------------------------

L2: Ø сессия-сдана(сидоров).

S4: сессия-сдана(сидоров).

-----------------------------------------

L3: ð.

 

Последовательность предложений { S1, S2, …, Sk } – вывод задачи.

Вывод L1, L2, L3 решает задачу, т.к. в теории резолюций доказана теорема, согласно которой:

S = { S1, S2, …, Sk } |= G <=> S, ØG |= ð.

 

Свойства резолюции:

Свойство корректности: S, ØG |= ð => S |= G.

Свойство полноты: S |= G => S, ØG |= ð.

Эти свойства не обеспечивают неограниченность возможности резолюции при доказательстве, поэтому основной проблемой, связанной с формальной логической системой, является проблема общей значимости. Проблема общей значимости связана с понятием интерпретации предложений.

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

· Каждому индивидууму из D ставится в соответствие имя из S.

· Каждому функтору из S ставится в соответствие функция, определенная на D.

· Каждому предикатному символу из S ставится в соответствие некоторое отношение на D.

Т.о., если говорят, что предложение из S истинно или ложно относительно выбранной интерпретации, то это означает, что истинно или ложно соответствующее высказывание из области D.

Определение 1. Предложение программы называется общезначимым, если оно выполняется во всех интерпретациях над произвольными областями D.

Проблема общей значимости частично разрешима для логики 1-го порядка. Это значит, что не существует алгоритма, позволяющего для произвольных S и D сделать вывод, справедливо ли отношение S |= G. Но имеются алгоритмы, которые устанавливают справедливость этого отношения (S |= G), если оно имеет место. Такие алгоритмы называются частично разрешающими процедурами, и к ним относятся процедуры, основанные на правиле резолюций. Т.о., если программа, не имеющая опровержения, подается на вход частично разрешающей процедуры, то вывод может оказаться бесконечным.

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