Сложность процедур доказательства теорем

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