Вывод, при котором поиск доказательства начинается с целевого утверждения. Выясняются условия, при которых целевое утверждение является выводимым. Эти условия принимаются за новые целевые утверждения и процесс поиска продолжается. В.О. заканчивается, когда все очередные условия оказываются аксиомами или процесс условий обрывается, не приведя к аксиомам. В.О. широко используется в интеллектуальных системах при поиске решений.