ОПЕРАТОРЫ СВЕДЕНИЯ ЗАДАЧИ К ПОДЗАДАЧАМ

результирующих, или дочерних, описаний задач. Это преобразование таково, что решение

всех дочерних задач обеспечивает решение исходной родительской задачи. Когда множество дочерних задач состоит из одного элемента, мы имеем простейший случай замены одной задачи другой, ей эквивалентной.

из которых применим. Применение каждого такого оператора порождает альтернативные множества

подзадач. Некоторые из этих подзадач могут оказаться неразрешимыми, так что нам придется перепробовать несколько операторов, чтобы построить такое множество, все члены которого разрешимы. Таким образом, снова возникает задача перебора.

истинны. Пусть  — утверждение, истинность которого мы хотим доказать,  множество посылок, которые

предполагаются верными. Тогда под  (читается «S при данном Т») мы будем понимать задачу доказательства утверждения  исходя из посылок Т. 

в том, чтобы ввести в исходную задачу новые посылки, а

затем сформулировать дополнительные задачи на доказательство этих новых посылок. Так, при редукции задачи  мы добавляем, скажем,  посылок и получаем следующее множество результирующих задач:

чтобы в каждый момент времени добавлялась лишь одна посылка. Тогда  сводится

к множеству 
Символы посылок  можно было бы рассматривать как переменные, принимающие значения из некоторого множества посылок. 

оператора сведения задачи. Этим переменным могут быть сразу же приданы

определенные значения в виде конкретных посылок (содержащих, возможно, новые переменные), но вместо этого их можно оставить в виде переменных, имея в виду, что конкретные значения могут быть им приданы в процессе дальнейшего сведения. Позже мы рассмотрим некоторые из предлагаемых подходов к выбору конкретных значений для посылок. Часто нам будет нужно в качестве частных значений выбрать более чем одно множество посылок, так что наше доказательство может вернуться назад и. пойти по другим альтернативным направлениям.