Искусственный интеллект

98 4.4. Вывод на основе правила резолюции -1 на {А, Стол) v -1 свободен (A) v -i свободен (В) v v -, переместить (А, В) v на (А, В), (4.171) на (А, В). (4.172) Таким образом, снова имеем истинные атомы на (А, В), на (В, Стол), на (С, Стол), на (D, Стол). Согласно правилу введения конъюнкции, вновь делаем заключение об истинности целевой формулы на (А, В) л на (В, Стол) л на (С, Стол) л на (D, Стол). На этом прямой вывод с использованием обобщенного правила резолюции завершен. Достоинством использования обобщенного правила резолюции для прямого вывода является способность выводить большее количество формул по сравнению с выводом на основе обобщенного правила модус поненс. В процессе вывода база знаний по-прежнему разрастается за счет занесения в нее вновь выводимых формул. Некоторые из этих формул могут оказаться ненужными для вывода целевой формулы.