разрешение 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»

Название «резолюция 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 выбранный литерал ограничен тем, который был введен в предложение последним. В простейшем случае такая функция выбора «последним пришел — первым вышел» может быть определена порядком, в котором записаны литералы, как в Prolog . Однако функция выбора в разрешении SLD более общая, чем в разрешении SL и в Prolog. Нет никаких ограничений на литерал, который может быть выбран. ${\displaystyle C_{i}\,}$

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

В клаузальной логике опровержение SLD демонстрирует, что входной набор предложений невыполним. Однако в логическом программировании опровержение SLD также имеет вычислительную интерпретацию. Верхнее предложение можно интерпретировать как отрицание конъюнкции подцелей . Вывод предложения из — это вывод с помощью обратного рассуждения нового набора подцелей с использованием входного предложения в качестве процедуры сокращения цели. Унифицирующая подстановка как передает входные данные из выбранной подцели в тело процедуры, так и одновременно передает выходные данные из головы процедуры в оставшиеся невыбранные подцели. Пустое предложение — это просто пустой набор подцелей, который сигнализирует о том, что начальная конъюнкция подцелей в верхнем предложении была решена. ${\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 является недетерминированным в том смысле, что оно не определяет стратегию поиска для исследования дерева поиска. Prolog ищет в глубину дерева, по одной ветви за раз, используя возврат, когда он сталкивается с узлом отказа. Поиск в глубину очень эффективен в использовании вычислительных ресурсов, но неполный, если пространство поиска содержит бесконечные ветви, и стратегия поиска ищет их в первую очередь, а не конечные ветви: вычисление не заканчивается. Возможны также другие стратегии поиска, включая поиск в ширину , наилучший первый и поиск ветвей и границ . Более того, поиск может выполняться последовательно, по одному узлу за раз, или параллельно, по многим узлам одновременно.

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

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

Пример

Дана логическая программа на языке Пролог :

в  :-  п .стр .

и цель высшего уровня:

в .

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

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

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

${\displaystyle p\,}$

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

${\displaystyle \neg q}$

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

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

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

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

в  :-  р .

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

Если пункт

п  :-  п .

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

СЛДНФ

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

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

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

Ссылки

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

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

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

• [1] Определение из бесплатного онлайн-словаря по вычислительной технике