Алгоритм резолюции

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

Процедуры логического вывода, основанные на правиле резолюции, действуют с использованием принципа доказательства путем установления противоречия, который описывался в конце раздела. Таким образом, чтобы показать, что KB ≠ α, мы покажем, что высказывание (KB ^ ¬α) является невыполнимым. Это можно сделать, доказав, что имеет место противоречие.

алгоритм резолюции приведен в листинге. Вначале высказывание (KB ^ ¬α) преобразуется в форму CNF.

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

• перестают вырабатываться какие-либо новые выражения, которые могли быть добавлены к существующим, и в этом случае из базы знаний KB не следует высказывание α;
• два противоположных друг другу выражения устраняются, в результате чего создается пустое выражение; в этом случае из базы знаний KB следует высказывание α.

Простой алгоритм резолюции для пропозициональной логики. Об этом говорит сайт https://intellect.icu . Функция PL-Resolveвозвращает множество всех возможных выражений, полученных путем устранения противоположных друг другу литералов из двух высказываний, которые поступают на ее вход

function PL-Resolution(KB, се) returns значение true или false

  inputs: KB, база знаний - высказывание в пропозициональной логике

  а, запрос - высказывание в пропозициональной логике

  clauses <— множество выражений, полученное после преобразования

  высказывания KB л —i(X в форму CNF

  new <— {}

  loop do

  for each d, Cj in clauses do

  resolvents <— PL-Resolve (Cl, Cj)

  if множество resolvents содержит пустое выражение

  then return true

  new <— new u resolvents

  if new с clauses then return false

  clauses <— clauses u new

Пустое выражение (дизъюнкция без дизъюнктов) эквивалентно высказыванию False, поскольку дизъюнкция является истинной, только если истинен по меньшей мере один из ее дизъюнктов. Еще один способ убедиться в том, что пустое выражение служит свидетельством противоречия, состоит в том, что, вернувшись к описанному выше процессу логического вывода, можно заметить, что пустое выражение возникает только после устранения двух взаимно противоположных единичных выражений, таких как Р и ¬Р.

Эту процедуру резолюции можно применить для формирования очень простого логического вывода в мире вампуса. Когда агент находится в квадрате [ 1,1 ], он не чувствует ветерка, поэтому в соседних квадратах не может быть ям. Соответствующая база знаний является следующей:

KB = R₂ ^ R₄ = (B_1,1 <=> (P_1,2 v P_2,1)) ^ ¬B_1,1

и требуется доказать высказывание α, которое, скажем, имеет вид ¬P_1,2. После преобразования высказывания (KB ^ ¬α) в форму CNF получим выражения. В нижнем ряду на этом рисунке показаны все выражения, полученные путем устранения противоположных друг другу литералов из всех пар выражений, приведенных в верхнем ряду. Затем после устранения литерала P_1,2, противоположного литералу ¬P_1,2, будет получено пустое выражение, показанное в виде небольшого квадрата.

Если я не полностью рассказал про алгоритм резолюции? Напиши в комментариях Надеюсь, что теперь ты понял что такое алгоритм резолюции и для чего все это нужно, а если не понял, или есть замечания, то не стесняйся, пиши или спрашивай в комментариях, с удовольствием отвечу. Для того чтобы глубже понять настоятельно рекомендую изучить всю информацию из категории Модели представления знаний