Статья 366

Здесь уже простое тестирование программ не в состоянии служить основой надежности программного обеспечения. Требуются иные процедуры и методы удостоверения правильности программ и отсутствия в них ошибок.
Еще одна сфера применения ЭВМ, где совершенно необходима уверенность в безошибочности программ доказательство математических теорем при помощи компьютеров. В самом деле, если результатом работы программы считается доказательство некоторого математического суждения, малейшая неточность при составлении программы например, просмотр одного-единственного возможного случая, способного изменить истинное значение доказываемого утверждения может обесценить всю программу в целом. Более того, высказывается точка зрения, согласно которой вообще нельзя доказывать математические теоремы на компьютерах. Рассмотрим этот аспект проблемы подробнее.
Одной из первых попыток применить компьютер при поиске доказательств математических теорем является программа Логик-Теоретик ЛТ известных специалистов по информатике С.