Автоматизоване міркування

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до навігації Перейти до пошуку

У інформатиці, зокрема в представленні знань і міркуваннях і металогіці, область автоматизованого міркування присвячена розумінню різних аспектів міркування. Вивчення автоматизованого міркування допомагає створювати комп'ютерні програми, які дозволяють комп'ютерам міркувати повністю або майже повністю автоматично. Хоча автоматизоване міркування вважається частиною сфери штучного інтелекту, воно також має зв'язок з теоретичною інформатикою та філософією.

Найрозвиненішими підгалузями автоматизованого міркування є автоматизоване доведення теорем (і менш автоматизована, але більш прагматична підгалузь інтерактивне доведення теорем[en]) і автоматизована перевірка доказів (розглядається як гарантовано правильне міркування за фіксованих припущень). Також проведена велика робота в міркуваннях за аналогією з використанням індукції та абдукції[en][1].

Інші важливі теми включають міркування в умовах невизначеності та немонотонні міркування. Важливою частиною поля невизначеності є аргументація, де на додаток до більш стандартного автоматизованого виведення застосовуються додаткові обмеження мінімальності та послідовності. Система OSCAR Джона Поллака[2] є прикладом автоматизованої системи аргументації, яка є більш конкретною, ніж просто автоматизоване доведення теорем.

Інструменти та методи автоматизованого міркування включають класичну логіку та обчислення, нечітку логіку, байєсівський висновок, міркування з принципів максимальної ентропії[en] та багато менш формальних спеціальних методів.

Ранні роки[ред. | ред. код]

Розвиток формальної логіки відіграв велику роль у сфері автоматизованого міркування, що само по собі призвело до розвитку штучного інтелекту. Формальний доказ — це доведення, у якому кожен логічний висновок перевіряється до фундаментальних аксіом математики. Надаються всі без винятку проміжні логічні кроки. До інтуїції не звертаються, навіть якщо переклад з інтуїції на логіку є рутинним. Таким чином, формальний доказ менш інтуїтивно зрозумілий і менш схильний до логічних помилок.[3]

Деякі вважають, що літня зустріч у Корнелії 1957 року, на якій зібралося багато логіків і вчених-комп'ютерників, є джерелом автоматизованого міркування або автоматизованого виведення.[4] Інші кажуть, що це почалося до цього з програми «Теоретик логіки»[en] Ньюелла, Шоу[en] та Саймона 1955 року або з впровадженням Мартіном Девісом у 1954 році процедури рішення Пресбургера (яка довела, що сума двох парних чисел є парною).[5]

Автоматизовані міркування, хоча і є важливою та популярною областю досліджень, пройшли через «зиму ШІ» у вісімдесятих та на початку дев'яностих. Однак згодом це поле досліджень відродилося. Наприклад, у 2005 році Microsoft почала використовувати технологію перевірки в багатьох своїх внутрішніх проєктах і планувала включити логічну специфікацію та мову перевірки у свою версію Visual C 2012 року[4].

Значні внески[ред. | ред. код]

Principia Mathematica була важливою роботою у формальній логіці, написаною Альфредом Нортом Уайтхедом і Бертраном Расселом. Principia Mathematica, що також означає Принципи математики, була написана з метою виведення всіх або деяких математичних виразів у термінах символічної логіки. «Principia Mathematica» спочатку була опублікована в трьох томах у 1910, 1912 та 1913 роках[6].

Теоретик логіки[en] (LT) була першою програмою, розробленою в 1956 році Алленом Ньюеллом, Кліффом Шоу[en] та Гербертом А. Саймоном, щоб «імітувати людські міркування» під час доведення теорем, і була продемонстрована на п'ятдесяти двох теоремах з розділу другої книги Principia Mathematica, доводячи тридцять — вісім з них.[7] Окрім доведення теорем, програма знайшла доведення однієї з теорем, який був більш елегантним, ніж той, який надали Уайтхед та Рассел. Після невдалої спроби опублікувати свої результати Ньюелл, Шоу та Герберт повідомили у своїй публікації 1958 року «Наступний прогрес у дослідженні операцій»:

«Зараз у світі є машини, які думають, вчаться і творять. Щобільше, їхня здатність робити це буде швидко зростати, доки (у видимому майбутньому) коло проблем, з якими вони можуть впоратися, не буде однаково широким з діапазоном, до якого був застосований людський розум»[8].

Системи з доведення[ред. | ред. код]

Довідник теореми Бойєра-Мура (NQTHM)
На розробку NQTHM[en] вплинули Джон Маккарті та Вуді Бледсо. Розпочатий у 1971 році в Единбурзі, Шотландія, це була повністю автоматична система з доведення теорем, створена за допомогою Pure Lisp. Основними аспектами NQTHM були:
  1. використання Lisp як робочої логіки.
  2. опора на принцип визначення для повних рекурсивних функцій.
  3. широке використання переписування та «символічної оцінки».
  4. індукційна евристика, заснована на невдачі символічного оцінювання.[9]
HOL Light
Написаний на OCaml, HOL Light[en] розроблено, щоб мати просту й чисту логічну основу та вільну реалізацію. По суті, це ще один помічник по доведенню для класичної логіки вищого порядку.[10]
Coq
Розроблений у Франції, Coq є ще одним автоматизованим помічником перевірки, який може автоматично витягувати виконувані програми зі специфікацій у вигляді вихідного коду Objective CAML або Haskell. Властивості, програми та доведення формалізовані тією ж мовою, що називається обчисленням індуктивних конструкцій (англ. Calculus of Inductive Constructions, CIC).[11]

Додатки[ред. | ред. код]

Автоматичне міркування найчастіше використовується для побудови автоматизованих доведень теорем. Часто, однак, для доведення теорем потрібні певні вказівки людини, щоб бути ефективними, і тому в більш загальному сенсі вони кваліфікуються як помічники для доведення. У деяких випадках такі довідники винайшли нові підходи до доведення теореми. Теоретик логіки[en] є хорошим прикладом цього. Програма знайшла доведення однієї з теорем Principia Mathematica, який був ефективнішим (вимагав менше кроків), ніж доведення, надане Вайтгедом і Расселом. Програми для автоматизованих міркувань застосовуються для вирішення все більшої кількості проблем з формальної логіки, математики та інформатики, логічного програмування, перевірки програмного та апаратного забезпечення, проєктування схем та багатьох інших. TPTP (Sutcliffe and Suttner 1998) — це бібліотека таких проблем, яка регулярно оновлюється. Також на конференції CADE[en] регулярно проводяться змагання серед автоматизованих доказників теорем (Pelletier, Sutcliffe and Suttner 2002); завдання для конкурсу вибираються з бібліотеки TPTP.[12]

Див. також[ред. | ред. код]

Конференції та семінари[ред. | ред. код]

Журнали[ред. | ред. код]

Спільноти[ред. | ред. код]

Примітки[ред. | ред. код]

  1. ↑ Defourneaux, Gilles, and Nicolas Peltier. «Analogy and abduction in automated deduction.» IJCAI (1). 1997.
  2. ↑ John L. Pollock
  3. ↑ C. Hales, Thomas «Formal Proof», University of Pittsburgh. Retrieved on 2010-10-19
  4. ↑ а б «Automated Deduction (AD)», [The Nature of PRL Project]. Retrieved on 2010-10-19
  5. ↑ Martin Davis (1983). The Prehistory and Early History of Automated Deduction. У Jörg Siekmann (ред.). Automation of Reasoning (1) — Classical Papers on Computational Logic 1957–1966. Heidelberg: Springer. с. 1—28. ISBN 978-3-642-81954-4. Here: p.15
  6. ↑ «Principia Mathematica», at Stanford University. Retrieved 2010-10-19
  7. ↑ «The Logic Theorist and its Children». Retrieved 2010-10-18
  8. ↑ Shankar, Natarajan Little Engines of Proof, Computer Science Laboratory, SRI International. Retrieved 2010-10-19
  9. ↑ The Boyer- Moore Theorem Prover. Retrieved on 2010-10-23
  10. ↑ Harrison, John HOL Light: an overview. Retrieved 2010-10-23
  11. ↑ Introduction to Coq. Retrieved 2010-10-23
  12. ↑ Automated Reasoning, Stanford Encyclopedia. Retrieved 2010-10-10

Посилання[ред. | ред. код]

Отримано з https://uk.wikipedia.org/w/index.php?title=Автоматизоване_міркування&oldid=40608591