Иллюстрированный самоучитель по введению в экспертные системы


Принцип резолюций - часть 2


/p>

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

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

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

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




Начало  Назад  Вперед



Книжный магазин