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

В обратном выводе все делается наоборот. На первом шаге обратного вывода подбирается правило вывода, следствием которого является целевая формула, а условие может быть образовано из формул начальной базы знаний, с использованием, если это необходимо, унификации. Унифицированные формулы, входящие в условие, принимаются за новые целевые формулы (обычно называемые подцелевыми формулами) и все повторяется сначала, но уже для каждой их них. И так до тех пор, пока все унифицированные подцелевые формулы не окажутся аксиомами, входящими в начальную базу знаний. При выводе на основе использования обобщенного правила модус поненс, унификации и хорновских формул используется только один тип правила, поэтому нет необходимости осуществлять выбор подходящего правила вывода. Это типизирует процедуры прямого и обратного вывода, превращая их в итеративную процедуру выполнения однотипных шагов. Рассмотрим прямой и обратный вывод на простых примерах из среды кубиков.