Разрешение 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» было дано Маартеном ван Эмденом неназванному правилу вывода, введенному Робертом Ковальски . ^[1] Его название происходит от резолюции SL, ^[2]что является одновременно обоснованным и полным опровержением для неограниченной клаузальной формы логики. «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 демонстрирует, что входной набор предложений невыполним. Однако в логическом программировании опровержение 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  .

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

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

$q\lor \neg p$

$p\,$

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

$\neg q$

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

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

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

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

q   :-   р  .

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

Если пункт

п   :   -п  .

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

СЛНФ [ править ]

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

См. также [ править ]

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

Ссылки [ править ]

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

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

Внешние ссылки [ править ]

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

[1] Роберт Ковальски Логика предикатов как язык программирования , памятка 70, Департамент искусственного интеллекта, Эдинбургский университет. 1973. Также в материалах Конгресса ИФИП, Стокгольм, North Holland Publishing Co., 1974, стр. 569–574.

[2] Роберт Ковальски и Дональд Кюнер, Линейное разрешение с искусственным интеллектом с функцией выбора , Vol. 2, 1971, стр. 227–60.

[3] Кшиштоф Апт и Маартен ван Эмден, Вклад в теорию логического программирования , Журнал Ассоциации вычислительной техники . Том, 1982 г. - портал.acm.org

[1]

[2]

[3]