Студопедия
Новини освіти і науки:
МАРК РЕГНЕРУС ДОСЛІДЖЕННЯ: Наскільки відрізняються діти, які виросли в одностатевих союзах


РЕЗОЛЮЦІЯ: Громадського обговорення навчальної програми статевого виховання


ЧОМУ ФОНД ОЛЕНИ ПІНЧУК І МОЗ УКРАЇНИ ПРОПАГУЮТЬ "СЕКСУАЛЬНІ УРОКИ"


ЕКЗИСТЕНЦІЙНО-ПСИХОЛОГІЧНІ ОСНОВИ ПОРУШЕННЯ СТАТЕВОЇ ІДЕНТИЧНОСТІ ПІДЛІТКІВ


Батьківський, громадянський рух в Україні закликає МОН зупинити тотальну сексуалізацію дітей і підлітків


Відкрите звернення Міністру освіти й науки України - Гриневич Лілії Михайлівні


Представництво українського жіноцтва в ООН: низький рівень культури спілкування в соціальних мережах


Гендерна антидискримінаційна експертиза може зробити нас моральними рабами


ЛІВИЙ МАРКСИЗМ У НОВИХ ПІДРУЧНИКАХ ДЛЯ ШКОЛЯРІВ


ВІДКРИТА ЗАЯВА на підтримку позиції Ганни Турчинової та права кожної людини на свободу думки, світогляду та вираження поглядів



Контакти
 


Тлумачний словник
Авто
Автоматизація
Архітектура
Астрономія
Аудит
Біологія
Будівництво
Бухгалтерія
Винахідництво
Виробництво
Військова справа
Генетика
Географія
Геологія
Господарство
Держава
Дім
Екологія
Економетрика
Економіка
Електроніка
Журналістика та ЗМІ
Зв'язок
Іноземні мови
Інформатика
Історія
Комп'ютери
Креслення
Кулінарія
Культура
Лексикологія
Література
Логіка
Маркетинг
Математика
Машинобудування
Медицина
Менеджмент
Метали і Зварювання
Механіка
Мистецтво
Музика
Населення
Освіта
Охорона безпеки життя
Охорона Праці
Педагогіка
Політика
Право
Програмування
Промисловість
Психологія
Радіо
Регилия
Соціологія
Спорт
Стандартизація
Технології
Торгівля
Туризм
Фізика
Фізіологія
Філософія
Фінанси
Хімія
Юриспунденкция






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

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

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




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

<== попередня сторінка | наступна сторінка ==>
Різновиди інтелектуальних систем | Експертні системи.

Не знайшли потрібну інформацію? Скористайтесь пошуком google:

 

© studopedia.com.ua При використанні або копіюванні матеріалів пряме посилання на сайт обов'язкове.


Генерація сторінки за: 0.005 сек.