• Гідрологія і Гідрометрія
• Господарське право
• Економіка будівництва
• Економіка природокористування
• Економічна теорія
• Земельне право
• Історія України
• Кримінально виконавче право
• Медична радіологія
• Методи аналізу
• Міжнародне приватне право
• Міжнародний маркетинг
• Основи екології
• Предмет Політологія
• Соціальне страхування
• Технічні засоби організації дорожнього руху
• Товарознавство продовольчих товарів

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

Історичний огляд робіт в області ШІ.

Серед найважливіших класів задач, які ставилися перед ИИ з моменту його зародження як наукового напрямку (із середини 50-х років ХХ століття), варто виділити наступні важко формалізуємі задачі, важливі й для задач робототехніки: доказ теорем, керування роботами, розпізнавання зображень, машинний переклад і розуміння текстів природною мовою, ігрові програми, машинна творчість (синтез музики, віршів, текстів).

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

В 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. До числа найбільш популярних традиційних мов програмування для створення ІС варто також віднести С++ і Паскаль.

Читайте також:

1. Аудиторські докази щодо тверджень керівництва у фінансових звітах отримуються безпосередньо в процесі проведення тестів контролю та процедур по суті.
2. Аудиторські докази.
3. Аудиторські докази: поняття та процедури отримання
4. Валідація НАССР- отримання об'єктивного доказу того, що елементи НАССР-плану результативні.
5. Види доказів у господарському судочинстві
6. Види доказів у господарському судочинстві
7. Види доказу
8. Види процедур отримання аудиторських доказів за їх типом
9. Види процедур отримання аудиторських доказів за їх характером
10. Використання матеріалів ОРД як приводів і підстав для порушення кримінальної справи, проведення невідкладних слідчих дій та як доказів у кримінальних справах
11. Витребування доказів є правом, а не обовязком судді.
12. Витребування, дослідження і оцінка доказів.

Переглядів: 646