68
правок
Изменения
м
Нет описания правки
<tex>\phi(A, B, t) = \exists R \, [\phi(A, R, t-1) \land \phi(R, B, t-1)]</tex>.
Заметим, что данная формула имеет экспоненциальный размер, поэтому так как за один шаг рекурсии длина пути уменьшается на одни, а размер формулы удваивается. Поэтому воспользуемся квантором <tex>\forall</tex> и перепишем её следующим образом:
<tex>\phi(A, B, t) = \exists R \,\forall U \,\forall V \, \{\phi(U, V, t-1) \lor [\neg(U = A \land V = R) \land \neg(U = R \land V = B)]\}</tex>.
