Разрешение SLD

Правило логического программирования

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Вычислительная интерпретация разрешения SLD

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

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

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

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

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

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

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

Пример

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

д  :-  п .п .

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

q .

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

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

${\displaystyle q\lor \neg p}$

${\displaystyle p\,}$

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

${\displaystyle \neg q}$

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

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

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

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

q  :-  р .

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

Если пункт

п  :  -п .

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

СЛНФ

SLDNF ^[3] — это расширение разрешения SLD, позволяющее рассматривать отрицание как отказ . В SLDNF предложения цели могут содержать отрицание в виде литералов отказа, скажем, формы , которую можно выбрать, только если они не содержат переменных. Когда выбирается такой литерал без переменных, предпринимается попытка поддоказательства (или подвычисления), чтобы определить, существует ли опровержение SLDNF, начиная с соответствующего неотрицательного литерала в качестве верхнего предложения. Выбранная подцель успешна, если дополнительное доказательство не удалось, и она не удалась, если дополнительное доказательство было успешным. ${\displaystyle not(p)\,}$ ${\displaystyle p\,}$ ${\displaystyle not(p)\,}$

Смотрите также

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

Рекомендации

1. Роберт Ковальски Логика предикатов как язык программирования, памятка 70, Департамент искусственного интеллекта, Эдинбургский университет. 1973. Также в материалах Конгресса ИФИП, Стокгольм, North Holland Publishing Co., 1974, стр. 569–574.
2. Роберт Ковальски и Дональд Кюнер, Линейное разрешение с искусственным интеллектом с функцией выбора , Vol. 2, 1971, стр. 227–60.
3. Кшиштоф Апт и Маартен ван Эмден, Вклад в теорию логического программирования, Журнал Ассоциации вычислительной техники . Том, 1982 г. - портал.acm.org

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

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

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