Искусственный интеллект - стр. 7
Как уже было упомянуто, основы формальной логики заложил ещё в античные времена Аристотель, однако потом до начала XX века эта методология использовалась учёными без какого-либо развития. Математики пытались как-то формализовать научный метод, и даже было произведено несколько интересных попыток. Немецкие математики и логики Георг Кантор и Готлоб Фреге фактически стали отцами наивной теории множеств и теории предикатов первого порядка соответственно. Эти теории позволяли формализовать очень многое, однако страдали от важного недостатка – противоречивости. И только в 1910–1913 гг. английские математики и философы Бертран Рассел и Альфред Уайтхед опубликовали трёхтомную работу «Принципы математики», где они ввели теорию типов как инструмент для более точной формализации основ математики, в которой невозможно было сформулировать парадокс Рассела о «множестве всех множеств». Именно после этой книги развитие математики пошло семимильными шагами, в результате чего сделали свои открытия Курт Гёдель, Алонзо Чёрч, Алан Тьюринг и многие другие замечательные учёные. Так что в историческом ряду развития формальной логики стоят такие личности, как Аристотель, Г. Кантор, Г. Фреге, Б. Рассел, А. Уайтхед и К. Гёдель.
После того как в 1931 г. австрийский логик Курт Гёдель опубликовал свои работы, в которых было приведено доказательство его знаменитых теорем о неполноте, начались исследования в этом направлении. Многие из них были чисто философскими, однако две примечательные работы легли в основу всей современной вычислительной техники. Первая – лямбда-исчисление Алонзо-Чёрча, описанное в его теперь уже знаменитой статье 1936 г., в которой он показал существование неразрешимых задач. Параллельно ему Алан Тьюринг переформулировал теорему Гёделя и, пытаясь решить «проблему разрешения» Давида Гильберта, разработал формализм в виде гипотетического устройства, которое впоследствии стало носить название «машины Тьюринга».
Обобщение достижений А. Чёрча и А. Тьюринга привело к формулированию тезиса Чёрча-Тьюринга, который, являясь эвристическим утверждением, гласит, что для любой алгоритмически вычислимой функции существует вычисляющая её значения машина Тьюринга. Этот тезис постулирует эквивалентность между интуитивным понятием алгоритмической вычислимости и строго формализованными понятиями частично рекурсивной функции (по Чёрчу), или функции, вычислимой на машине Тьюринга (по Тьюрингу). Тезис невозможно строго доказать или опровергнуть ввиду того, что интуитивное понятие алгоритмической вычислимости строго не определено. Однако этот тезис в совокупности с теорией вычислений сегодня лежит в основе алгоритмического решения задач и, как следствие, имеет непосредственное применение в рамках искусственного интеллекта.