Резолюция

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

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

Начнем с использования простой версии правила резолюции в мире вампуса. Рассмотрим шаги, ведущие вверх на рисунке, а: агент возвращается из квадрата [2,1] в квадрат [ 1,1 ], а затем переходит в квадрат [1,2], где он чувствует неприятный запах, но не ощущает ветерка. Введем следующие дополнительные факты в базу знаний:

R₁₁: ¬B_1,2

R₁₂: B_1,2 <=> (P_1,1 v P_2,2 v P_1,3)

С помощью того же процесса, который привел к получению высказывания R₁₀, приведенного выше, мы теперь можем сделать заключение об отсутствии ям в квадратах [2,2] и [1,3] (напомним, что в отношении квадрата [1,1] уже известно, что в нем нетям):

R₁₃: ¬P_2,2

R₁₄: ¬P_1,3

Кроме того, можно применить к высказыванию R₃ правило удаления двухсторонней импликации, после чего применить к полученному результату в сочетании с высказыванием R₅ правило отделения, чтобы выяснить тот факт, что по меньшей мере в одном из квадратов [1,1], [2,2] или [3,1] есть яма:

R₁₅: P_1,1 v P_2,2 v P_3,1

Именно здесь возникают условия, позволяющие впервые использовать правило резолюции (правило устранения противоречия): литерал ¬P_2,2 в высказывании R₁₃, противоположный литералу P_2,2 в высказывании R₁₅, устраняется, что приводит

к получению следующего высказывания:

Соответствующий ход рассуждения можно выразить словами таким образом: если по меньшей мере в одном из квадратов [1,1], [2,2] или [3,1] имеется яма, но ее нет в квадрате [2,2], то яма должна быть, по крайней мере, в квадрате [1,1] или [3,1]. Об этом говорит сайт https://intellect.icu . Аналогичным образом, устраняется литерал ¬P_1,1 в высказывании R₁₆противоположный литералу P_1,1 в высказывании R₁₆, что приводит к получению следующего высказывания:

R17: R3,1

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

 

где каждое из выражений l представляет собой литерал, а выражения l_i и m являютсявзаимно обратными литералами (т.е. такими литералами, что один из них является отрицанием другого). Таким образом, в правиле единичной резолюции беретсявыражение (дизъюнкция литералов) и еще один литерал, после чего формируется новое выражение. Обратите внимание на то, что этот единственный литерал может рассматриваться как дизъюнкция из одного литерала, называемая также единичным выражением. Правило единичной резолюции может быть также обобщено до правила полной резолюции:

 

где l_i и m_j -- взаимно обратные литералы. Если бы мы имели дело только с выражениями, имеющими длину два, то могли бы записать данное правило следующим образом:

 

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

 

 

Процесс применения правила резолюции связан с необходимостью выполнения еще одного формального требования: результирующее высказывание должно содержать только по одной копии каждого литерала11. Операция удаления дополнительных копий литералов называется факторизацией. Например, после удаления противоположных друг другу литералов в выражениях (A v B) и (A v ¬B) будет получено выражение (A vA), которое следует сократить до A

 

Непротиворечивость правила резолюции можно легко доказать, рассматривая литералl_i- Если литерал l_i является истинным, то литерал лг, является ложным, и поэтому выражение m₁ v … v m_j-1 v m_j+1 v … v m_n должно быть истинным, поскольку дано, что истинно выражение m₁ v … v m_n. Если литерал l_i является ложным, то должно быть истинным выражение l₁ v … v l_i-1 v l_i-1 v … v l_k, поскольку дано, что истинно выражениеl₁ v … v l_k. Итак, литерал l_i является либо истинным, либо ложным, поэтому справедливо одно или второе из этих заключений, а именно это утверждается в правиле резолюции.

Еще более привлекательным свойством правила резолюции является то, что оно образует основу для семейства полных процедур логического вывода. Любой полный алгоритм поиска, в котором применяется только правило резолюции, позволяет вывести любое заключение, которое следует из любой базы знаний в пропозициональной логике. Тем не менее необходимо сделать одно предупреждение: правило резолюции является полным только в узком смысле этого понятия. Если известно, что высказывание А истинно, правило резолюции нельзя использовать для автоматического формирования следствия A v B. Однако в этом случае правилом резолюции можно воспользоваться для поиска ответа на вопрос, является ли истинным высказывание A v B. Это свойство правила резолюции называется полнотой опровержения (refutation completeness) и означает, что правило резолюции может всегда использоваться либо для подтверждения, либо для опровержения какого-то высказывания, но его нельзя применять для перебора всех истинных высказываний. В следующих двух подразделах описано, как может использоваться правило резолюции для осуществления логического вывода.

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

Из статьи мы узнали кратко, но содержательно про резолюция