Разрешение SLD

Разрешение SLD ( выборочное линейное разрешение определенных предложений) — это основное правило вывода, используемое в логическом программировании . Это уточнение резолюции , которое является одновременно обоснованным и полным опровержением положений Хорна .

Правило вывода SLD

Учитывая целевое предложение, представленное как отрицание проблемы, которую необходимо решить:

$\neg L_{1}\lor \cdots \lor \neg L_{i}\lor \cdots \lor \neg L_{n}$

с выбранным литералом $\neg L_{i}$и входное определенное предложение :

$L\lor \neg K_{1}\lor \cdots \lor \neg K_{m}$

чей положительный литерал (атом) $L\,$ объединяется с атомом $L_{i}\,$ выбранного литерала $\neg L_{i}\,$, разрешение SLD создает еще одно предложение цели, в котором выбранный литерал заменяется отрицательными литералами входного предложения и объединяющей заменой. $\theta \,$ применяется:

$(\neg L_{1}\lor \cdots \lor \neg K_{1}\lor \cdots \lor \neg K_{m}\ \lor \cdots \lor \neg L_{n})\theta$

В простейшем случае, в логике высказываний, атомы $L_{i}\,$ и $L\,$ тождественны, а объединяющая замена $\theta \,$ является пустым. Однако в более общем случае объединяющая замена необходима, чтобы сделать два литерала идентичными.

Происхождение названия «СЛД»

Название «резолюция SLD» было дано Маартеном ван Эмденом неназванному правилу вывода, введенному Робертом Ковальски . Его название происходит от резолюции SL, что является одновременно обоснованным и полным опровержением для неограниченной клаузальной формы логики. «SLD» означает «резолюция SL с определенными положениями».

И в SL, и в SLD буква «L» означает тот факт, что доказательство разрешения может быть ограничено линейной последовательностью предложений:

$C_{1},C_{2},\cdots ,C_{l}$

где "верхнее предложение" $C_{1}\,$ является входным предложением, а все остальные предложения $C_{i+1}\,$ является резольвентным, одним из родителей которого является предыдущее предложение $C_{i}\,$. Доказательство является опровержением, если последнее предложение $C_{l}\,$ это пустое предложение.

В SLD все предложения в последовательности являются предложениями цели, а другой родительский элемент — входным предложением. При разрешении SL другим родительским элементом является либо входное предложение, либо предложение-предок, расположенное ранее в последовательности.

И в SL, и в SLD буква «S» означает тот факт, что единственный литерал, разрешенный в любом предложении. $C_{i}\,$ это тот, который однозначно выбирается с помощью правила выбора или функции выбора. В разрешении SL выбранный литерал ограничивается тем, который был введен в предложение последним. В простейшем случае такая функция выбора «последним пришел — первым вышел» может определяться порядком записи литералов, как в Прологе . Однако функция выбора в разрешении SLD более общая, чем в разрешении SL и в Прологе. Нет ограничений на выбор литерала.

разрешения

В клаузальной логике опровержение SLD демонстрирует, что входной набор предложений невыполним. Однако в логическом программировании опровержение SLD также имеет вычислительную интерпретацию. Верхнее предложение $\neg L_{1}\lor \cdots \lor \neg L_{i}\lor \cdots \lor \neg L_{n}$ можно интерпретировать как отрицание конъюнкции подцелей $L_{1}\land \cdots \land L_{i}\land \cdots \land L_{n}$. Вывод пункта $C_{i+1}\,$ от $C_{i}\,$ — это выведение посредством обратного рассуждения нового набора подцелей с использованием входного предложения в качестве процедуры сокращения цели. Объединяющая замена $\theta \,$ обе передают входные данные выбранной подцели в тело процедуры и одновременно передают выходные данные из головы процедуры в оставшиеся невыбранные подцели. Пустое предложение — это просто пустой набор подцелей, который сигнализирует о том, что первоначальное соединение подцелей в верхнем предложении решено.

Стратегии разрешения SLD

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

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

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

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

Пространство поиска разрешения SLD представляет собой ИЛИ-дерево, в котором разные ветви представляют альтернативные вычисления. В случае программ пропозициональной логики SLD можно обобщить так, что пространство поиска представляет собой дерево «и-или» , узлы которого помечены одиночными литералами, представляющими подцели, а узлы соединяются либо конъюнкцией, либо дизъюнкцией. В общем случае, когда совместные подцели имеют общие переменные, представление дерева и/или более сложное.

Пример

Учитывая логическую программу:

q :- p.
p.

и цель верхнего уровня:

q.

пространство поиска состоит из одной ветви, в которой q сводится к p который сводится к пустому набору подцелей, сигнализируя об успешном вычислении. При этом программа настолько проста, что здесь нет никакой роли функции выбора и нет необходимости в каком-либо поиске.

В клаузальной логике программа представлена ​​набором предложений:

$q\lor \neg p$

$p\,$

а цель верхнего уровня представлена ​​предложением цели с одним отрицательным литералом:

$\neg q$

Пространство поиска состоит из единственного опровержения:

$\neg q,\neg p,{\mathit {false}}$

где ${\mathit {false}}\,$ представляет собой пустое предложение.

Если бы в программу был добавлен следующий пункт:

q :- r.

тогда в пространстве поиска появится дополнительная ветвь, листовой узел которой r является отказным узлом. В Прологе, если бы это предложение было добавлено в начало исходной программы, то Пролог использовал бы порядок, в котором написаны предложения, для определения порядка, в котором исследуются ветви пространства поиска. Пролог сначала попробовал эту новую ветвь, но потерпел неудачу, а затем вернулся, чтобы исследовать единственную ветвь исходной программы и добился успеха.

Если пункт

p :- p.

теперь были добавлены в программу, то дерево поиска будет содержать бесконечную ветвь. Если бы это предложение было выполнено первым, то Пролог вошел бы в бесконечный цикл и не нашел бы успешной ветви.

СЛНФ

СЛНФ является расширением резолюции SLD для работы с отрицанием как с неудачей . В SLDNF предложения целей могут содержать отрицание в виде литералов отказа, скажем, в форме $not(p)\,$, которые можно выбрать, только если они не содержат переменных. Когда выбирается такой литерал без переменных, предпринимается попытка поддоказательства (или подвычисления), чтобы определить, существует ли опровержение SLDNF, начиная с соответствующего неотрицательного литерала. $p\,$ как верхнее предложение. Выбранная подцель $not(p)\,$ завершается успешно, если дополнительное доказательство терпит неудачу, и оно терпит неудачу, если дополнительное доказательство оказывается успешным.

См. также

• Джон Алан Робинсон

Ссылки

• Жан Галье , SLD-разрешение и логическое программирование, глава 9 книги «Логика для информатики: основы автоматического доказательства теорем» , онлайн-версия 2003 г. (бесплатная загрузка), первоначально опубликованная Wiley, 1986 г.
• Джон К. Шепердсон, SLDNF-Резолюция с равенством , Журнал автоматизированного рассуждения 8: 297-306, 1992; определяет семантику, относительно которой SLDNF-разрешение с равенством является правильным и полным

Внешние ссылки

• [1] Определение из бесплатного онлайн-словаря по информатике.