Как начинался компьютер
Компьютерная революция
Двоичный код
Разработки военных лет
Интегральные микросхемы
Микрокомпьютер
Персоны
Сеть
Язык компьютера
Развитие ПО
Гибкие системы
Средства разработки
Информатика
Вычислительная наука
Операционные системы
Искусственный интеллект
Предыстория
Поиск
Знания и рассуждения
Логика
Робототехника
 

 
Резолюция Печать

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

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

R11: ¬B1,2

R12: B1,2 <=> (P1,1 v P2,2 v P1,3)

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

R13: ¬P2,2

R14: ¬P1,3

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

R15: P1,1 v P2,2 v P3,1

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

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

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

R17: R3,1

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

Image

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

Image

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

Image

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

Image

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

Непротиворечивость правила резолюции можно легко доказать, рассматривая литерал li- Если литерал li является истинным, то литерал лг, является ложным, и поэтому выражение m1 v v mj-1 v mj+1 v v mn должно быть истинным, поскольку дано, что истинно выражение m1 vv mn. Если литерал li является ложным, то должно быть истинным выражение l1 v v li-1 v li-1 v v lk, поскольку дано, что истинно выражение l1 vv lk. Итак, литерал li является либо истинным, либо ложным, поэтому справедливо одно или второе из этих заключений, а именно это утверждается в правиле резолюции.

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