Подобная ситуация приятна, но редко встречается в действительности. При решении любой задачи, даже если заранее известен ее ответ, к которому надо стремиться (для школьника эта ситуация с подглядыванием в ответ до решения задачи весьма типична), мы не видим перед собой полного лабиринта возможностей. Мы пытаемся построить этот лабиринт, видя лишь начальные «площадки лабиринта» и не зная, что лежит между ними и «целевыми площадками». В нашем примере мы стоим на начальной площадке, в вершине ?1
, и не знаем, куда идти. Мы делаем попытку перейти в ?2 (т.е. вывести утверждение), но видим, что этого нельзя сделать. Тогда мы движемся в сторону утверждения ?3 и обнаруживаем, что его доказательство возможно. Теперь в нашем распоряжении две площадки лабиринта: ?1 и ?3. Из ?3 можно двигаться в четырех направлениях. Одно из них, ведущее назад к ?1, интереса не представляет. Попытка продвинуться к ?2 и ?5 оказывается успешной. Возникает новый фронт достигнутых площадок (доказанных утверждений). Теперь его образуют ?2, ?3 и ?5. Площадка ?1 исключается из активного фронта, так как использованы все связи этой площадки с другими площадками лабиринта. На следующем шаге достигаются площадки ?4 и ?6. Наличие среди доказанных выражений целевого ?6 позволяет завершить процесс доказательства. После этого можно произвести «чистку», в результате которой останется лишь тот путь, который кратчайшим образом приводит от начального утверждения ?1 к целевому ?6.На примере мы описали процедуру, которая, как легко видеть, носит универсальный характер и пригодна для поиска пути вывода в лабиринтах произвольного типа. Эта процедура известна среди специалистов под названием
Возможен и другой способ поиска доказательства. Он носит название
Различие между прямой и обратной волной состоит в том, что они порождают в процессе своего движения различные промежуточные «фронты» площадок, что приводит к различному числу шагов при поиске. Часто используется смешанный метод вывода, при котором одновременно движутся прямая и обратная волны. При встрече этих волн формируется путь вывода от начальных аксиом к целевым выражениям.
Несколько иной разновидностью схем вывода являются так называемые
В знаменитом рассказе «Убийство на улице Морг» Эдгара По сыщик-любитель Огюст Дюпен помещает в газете объявление о находке орангутанга, который, по слухам, принадлежит матросу мальтийского корабля. На вопрос о причинах такого объявления Огюст Дюпен отвечает следующим образом: