Доказ теорем.

Вивчення прийомів доказу теорем зіграло важливу роль у розвитку ШІ. Формалізація дедуктивного процесу з використанням логіки предикатів допомагає глибше зрозуміти деякі компоненти міркувань. Багато неформальних задач, наприклад, медична діагностика, допускають формалізацію як задачу на доказ теорем. Пошук доказу математичної теореми вимагає не лише зробити дедукцію, виходячи з гіпотез, але також створити інтуїтивні здогади й гіпотези про те, які проміжні твердження варто довести для виводу доказу основної теореми.

В 1954 році А. Ньюэлл задумав створити програму для гри в шахи. Дж. Шоу й Г. Саймон об'єдналися в роботі по проекту Ньюелла й в 1956 році вони створили мову програмування ІPL-І (попередник LіSPа) для роботи із символьною інформацією. Їхніми першими програмами стала програма LT (Logіc Theorіst) для доказу теорем і числення висловлень (1956 рік), а також програма NSS (Newell, Shaw, Sіmon) для гри в шахи (1957 рік). LT й NSS призвели до створення А. Ньюеллом, Дж. Шоу і Г. Саймоном програми GPS (General Problem Solver) в 1957-1972 роках. Програма GPS моделювала використовувані людиною загальні стратегії рішення задач і могла застосовуватись для рішення шахових і логічних задач, доказу теорем, граматичного розбору речень, математичного інтегрування, головоломок типу "Ханойська вежа" і т.д. Процес роботи GPS відтворює методи рішення задач, використуємих людиною: висуваються підцілі, що наближають до рішення, застосовується евристичний метод (один, другий і т.д. ), поки не буде отримано рішення. Спроби припиняються, якщо одержати рішення не вдається. Програма GPS могла вирішувати лише відносно прості задачі. Її універсальність досягалася за рахунок ефективності. Спеціалізовані "вирішувачі задач" - STUDENT (Bobrov, 1964) і ін. краще проявляли себе при пошуку рішення у своїх предметних областях. GPS виявилася першою програмою (написана мовою ІPL-V), у якій передбачалося планування стратегії рішення задач.

Для рішення важко формалізуємих задач і, зокрема, для роботи зі знаннями були створені мови програмування для задач ШІ: LІSP (1958 рік, J. MacCatthy), Пролог (1975-79 роки, D. Warren, F. Pereіra), ІнтерLіSP, FRL, KRL, SMALLTALK, OPS5, PLANNER, QA4, MACSYMA, REDUCE, РЕФАЛ, CLІPS. До числа найбільш популярних традиційних мов програмування для створення ІС варто також віднести С++ і Паскаль.