Новая философская энциклопедия. Том первый

ДОКАЗАТЕЛЬСТВ ТЕОРИЯ устранения вершин окольных путей обладает свойством полной недетерминированности: независимо от порядка применения операций за конечное число шагов получается нормшшзованный вывод. Но сам результирующий вывод существенно зависит от порядка применения шагов. В последнее время на стыках между теорией доказательств и информатикой появились новые классы результатов. Во-первых, выяснилось, что структуры доказательств и структуры извлекаемых из них построений, записанных на алгоритмическом языке достаточно высокого уровня (допускающем работу с значениями высших типов; так что Pascal и С этим требованиям не удовлетворяют), тесно связаны. Построение мономорфно вкладывается в доказательство, а часть доказательства, получающаяся отбрасыванием шагов и формул, нужных лишь для обоснования результата, изоморфна программе. Далее, были рассмотрены соотношения между преобразованиями доказательств и скрытых в них программ. Оказалось, что нормализация соответствует вычислению программы в символьной форме (т. е. когда.проделываются все вычисления и преобразования выражений, которые не зависят от входных данных). Оптимизирующие преобразования программ в свою очередь подсказали новые классы преобразований доказательств, ориентированные на устранение избыточностей. Лит.: Клини С. К. Введение в метаматематику. М., 1957; Та- кеути Г. Теория доказательств. М., 1978. Я. Н. Непейвода, В, А. Смирнов