Обратный вывод на основе опровержения и обобщенной резолюции

 

Как уже отмечалось, вывод истинности целевой формулы может осуществляться по очереди литерал за литералом. Поэтому рассмотрим его только для одного литерала на (А, В) целевой формулы (4.157). Опровержением литерала на (А, В) является литерал на (А, В). Обратный вывод начинается именно с этого литерала. Для того чтобы можно было детально проследить процесс вывода, будем записывать на каждом шаге вывода с помощью обобщенной резолюции три формулы — две исходные и резольвенту, нумеруя по ходу вывода получаемые резольвенты, а также указывая для каждого шага используемые подстановки и подчеркивая те литералы, которые в резольвенту не попадают:

на (А, В); (4.173)

на (А, Стол) свободен (A) свободен (В)

переместить (А, В) на (А, В); (4.174)

на (А, Стол) свободен (A) свободен (В)

переместить (А, В); (4.175)

на (А, Стол) свободен (A) свободен (В)

переместить (А, В); (4.176)

на (А, Стол) свободен (A) свободен (В)

переместить (А, В); (4.177)

на (А, Стол) свободен (A) свободен (В); (4.178)

на (А, Стол) свободен (A) свободен (В); (4.179)

свободен (А); (4.180)

на (А, Стол) свободен (В); (4.181)

на (А, Стол) свободен (В); (4.182)

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

на (А, Стол); (4.183)

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

свободен (В); (4.184)

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

свободен (В); (4.185)

свободен (А); (4.186)

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

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

свободен (В); (4.188)

на (D, B) свободен (D)

переместить (D, Стол); (4.189)

на (D, B) свободен (D) свободен (В); (4.190)

на (D, B) свободен (D) свободен (В); (4.191)

свободен (D); (4.192)

на (D, B) свободен (В); (4.193)

на (D, B) свободен (В); (4.194)

на (D, B); (4.195)

свободен (В); (4.196)

свободен (В); (4.197)

свободен (В); (4.198)

Nil. (4.199)