Прямой вывод

Начнем с формулы (4.136), унифицируя которую получим следующие формулы:

на (А, С) свободен (А) переместить (А, Стол), (4.143)

на (D, В) свободен(D) переместить (D, Стол). (4.144)

На основании обобщенного правила модус поненс и формул (4.130), (4.134), (4.132), (4.135), (4.143), (4.144) делаем заключение о возможности выполнения действия по перемещению кубиков А и D на стол: истинны атомы переместить (А, Стол), переместить (D, Стол). Эти атомы помещаются в исходную базу знаний. Далее можно воспользоваться формулами (4.138), (4.139), унифицируя которые получим формулы

на (А, С) свободен (А) переместить (А, Стол) на (А, Стол), (4.145)

на (А, С) свободен (А) переместить {А, Стол) свободен (С), (4.146)

на (D, В) свободен (D) переместить (D, Стол) на (D, Стол), (4.147)

на (D, В) свободен (D) переместить (D, Стол) свободен (В). (4.148)

В результате кубики А и D оказались на столе. Кубики С и В никуда не перемещались и, согласно начальному состоянию, остались на столе. Используя формулу (4.137), получим унифицированную формулу

на (А, Стол) свободен (А) свободен (В) переместить (А, В). (4.149)

Наконец, воспользовавшись формулой (4.138), получим унифицированную формулу

на (А, Стол) свободен (А) свободен (В) переместить (А, В)

на (А, В) (4.150)

Рисунок 8 - Граф прямого вывода в среде кубиков

Таким образом, имеем истинные атомы на (А, В), на (В, Стол), на (С, Стол), на (D, Стол). Согласно правилу введения конъюнкции, делаем заключение об истинности целевой формулы на (А, В) на (В, Стол) на (С, Стол) на (D, Стол). На этом прямой вывод завершен. На рис. 4.2 показан граф вывода указанной целевой формулы. В процессе прямого вывода база знаний разрастается, в нее заносятся вновь выводимые формулы. Некоторые из них могут оказаться ненужными для вывода целевой формулы. Таких «лишних» формул может быть достаточно много. Например, на рис. 4.2 ненужной является формула свободен (С).