Искусственный интеллект

Компьютер представляет собой физическое устройство, состоящее из электронных микросхем, материальных накопителей информации, оборудования для её ввода и вывода и т.д., которое обеспечивает его функционирование как логического устройства, позволяющего представить доказательства в виде формальных выводов в некоторой дедуктивной системе и зафиксировать эти выводы на материальных носителях информации. Работоспособность аппаратных средств, отсутствие у оборудования ошибок и сбоев в работе можно проверить с помощью соответствующих тестирующих программ, перепроверки результатов тестовых вычислений на других компьютерах и т.д. Если работоспособность компьютера как физического и логического устройств сомнений не вызывает, то для проверки правильности необозримых доказательств и решений остаётся лишь убедиться в правильности соответствующих программ. На практике правильность программы (алгоритма) выявляется на этапе её прогона и проверки с помощью специальных тестов, подбор которых во многих случаях представляет собой далеко не тривиальную задачу. Такое тестирование, по-видимому, носит сугубо теоретический характер, так как в ходе него соотносятся два теоретических продукта - программа и полученные с её помощью результаты вычислений. Однако положительные тесты все же не могут гарантировать отсутствие логических ошибок в программе и служить доказательством её правильности. Проблема сдвигается в плоскость традиционных методов, поскольку удостовериться в формальном выполнении алгоритма и тем самым доказать формальную правильность программы может только человек. Рассматривая текст программы как статический математический объект, на который распространяются аксиомы и логико-математические правила вывода, разработчик должен «вручную» воспроизвести действия, строго соответствующие имеющемуся алгоритму. Если для создания программы был использован язык с обозримым алфавитом, то доказательство правильности программы оказывается обозримой процедурой и осуществить его не представляет особого труда. Обозримая программа в принципе способна совершить необозримое число шагов, проверить и вывести сколь угодно длинные формулы. Если же текст программы необозримый, то доказательство правильности такой программы оказывается задачей алгоритмически неразрешимой (так как вопрос о завершении, остановке произвольного вычисления остается открытым), которая не может быть реализована на компьютере. Понятно, что только в случае обозримости используемых программ, а также при наличии формального вывода в некоторой формальной дедуктивной системе степень строгости и эпистемологический статус математических утверждений, доказательство которых проведено с использованием современной вычислительной техники, нисколько не уступает результатам, полученным традиционным способом¹¹¹.

Эпистемологические особенности логики как формальной науки