Введение в экспертные системы

         

Обобщение резолюции



Таблица 8.1. Обобщение резолюции



Правило вывода

Обычная форма

Конъюнктивная нормальная форма

Modus ponens

(U

{¬U,Ф},{U}/{ф}

Modus fallens

(U

{¬U,ф},{-,ф}/{-U}

Сцепление

(UТаблица 8.1. Обобщение резолюции£)(U

{¬U,ф},{¬ф,£}/{¬U,£}

Слияние

(UТаблица 8.1. Обобщение резолюции ф)/ф

{U,ф},{¬U,ф}/{ф}

Reductio

(U,¬U)/ |

{¬U},{U}/{}

Обратите внимание на то, что противоречие в правиле, которое обычно обозначается значком 1, дает в результате пустую фразу— {}. Это означает, что предпосылки несовместимы. Если считать, что предпосылки описывают некоторое состояние предметной области, то такой набор предпосылок не может быть реально обеспечен в ней, т.е. такое состояние невозможно.

Главное, что нужно вынести из всего сказанного выше, что компонент автоматического доказательства теорем, который является основным компонентом большинства систем искусственного интеллекта и, в частности, языков программирования искусственного интеллекта, таких как PROLOG, является системой, опровержения резолюций. Для того чтобы доказать, что р следует из некоторого описания состояния (или теории) Т, нужно положить —р и попытаться доказать, что из этого предположения следует утверждение, противоречащее Т. Если это удастся сделать, то тем самым подтверждается утверждение р, а в противном случае оно опровергается.

В исчислении предикатов использование резолюций требует дополнительных усилий, поскольку в этом исчислении присутствуют переменные. Основная операция сопоставления в доказательстве теорем с помощью резолюций называется унификацией (подробное описание используемого при этом алгоритма читатель найдет, например, в работе Нильсона [Nilsson, 1980]). При сопоставлении дополняющих литералов отыскивается такая подстановка переменных, которая превращает оба выражения в идентичные.

Например, выражения БЕЖИТ_БЫСТРЕЕ_ЧЕМ(Х, улитка) и БЕЖИТ_БЫСТРЕЕ _ЧЕМ (черепаха, Y) превращаются в идентичные при подстановке {Х/черепаха, Y/улитка}. Такая подстановка называется унификатором. Наша цель — отыскать наиболее общую подстановку такого рода.



Содержание раздела