Доказательство теорем.

Изучение приемов доказательства теорем сыграло важную роль в развитии ИИ. Формализация дедуктивного процесса с использованием логики предикатов помогает глубже понять некоторые компоненты рассуждений. Многие неформальные задачи, например, медицинская диагностика, допускают формализацию как задачу на доказательство теорем. Поиск доказательства математической теоремы требует не только произвести дедукцию, исходя из гипотез, но также создать интуитивные догадки и гипотезы о том, какие промежуточные утверждения следует доказать для вывода доказательства основной теоремы.

В 1954 году А. Ньюэлл задумал создать программу для игры в шахматы. Дж. Шоу и Г. Саймон объединились в работе по проекту Ньюэлла и в 1956 году они создали язык программирования IPL-I (предшественник LISPа) для работы с символьной информацией. Их первыми программами стала программа LT (Logic Theorist) для доказательства теорем и исчисления высказываний (1956 год), а также программа NSS (Newell, Shaw, Simon) для игры в шахматы (1957 год). LT и NSS привели к созданию А. Ньюэллом, Дж. Шоу и Г. Саймоном программы GPS (General Problem Solver) в 1957-1972 годах

Программа GPS моделировала используемые человеком общие стратегии решения задач и могла применяться для решения шахматных и логических задач, доказательства теорем, грамматического разбора предложений, математического интегрирования, головоломок типа «Ханойская башня» и т. д. Процесс работы GPS воспроизводит методы решения задач, применяемые человеком: выдвигаются подцели, приближающие к решению, применяется эвристический метод (один, другой и т. д.), пока не будет получено решение. Попытки прекращаются, если получить решение не удается. Программа GPS могла решать только относительно простые задачи. Ее универсальность достигалась за счет эффективности. Специализированные «решатели задач» - STUDENT (Bobrov, 1964) и др. лучше проявляли себя при поиске решения в своих предметных областях. GPS оказалась первой программой (написана на языке IPL-V), в которой предусматривалось планирование стратегии решения задач.

В начале 70-х годов они опубликовали много данных подобного рода и предложили общую методику составления программ, моделирующих мышление.

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

На дальнейшие исследования в области ИИ большое влияние оказало появление метода резолюций Робинсона, основанного на доказательстве теорем в логике предикатов и являющегося исчерпывающим методом доказательства. При этом определение термина ИИ претерпело существенное изменение. Целью исследований, проводимых в направлении ИИ, стала разработка программ, способных решать "человеческие задачи". Так, один из видных исследователей ИИ того времени Р. Бенерджи в 1969 году писал: "Область исследований, обычно называемую ИИ, вероятно, можно представить как совокупность методов и средств анализа и конструирования машин, способных выполнять задания, с которыми до недавнего времени мог справиться только человек. При этом по скорости и эффективности машины должны быть сравнимы с человеком." Функциональный подход к направленности исследований по ИИ сохранился в основном до настоящего времени, хотя еще и сейчас ряд ученых, особенно психологов, пытаются оценивать результаты работ по ИИ с позиций их соответствия человеческому мышлению.

Для решения трудно формализуемых задач и, в частности, для работы со знаниями были созданы языки программирования для задач ИИ: LISP (1960 год, J. MacCatthy), Пролог (1975-79 годы, D. Warren, F. Pereira), ИнтерLISP, FRL, KRL, SMALLTALK, OPS5, PLANNER, QA4, MACSYMA, REDUCE, РЕФАЛ, CLIPS. К числу наиболее популярных традиционных языков программирования для создания ИС следует также отнести С++ и Паскаль.