Azərbaycanca AzərbaycancaБеларускі БеларускіDansk DanskDeutsch DeutschEspañola EspañolaFrançais FrançaisIndonesia IndonesiaItaliana Italiana日本語 日本語Қазақ ҚазақLietuvos LietuvosNederlands NederlandsPortuguês PortuguêsРусский Русскийසිංහල සිංහලแบบไทย แบบไทยTürkçe TürkçeУкраїнська Українська中國人 中國人United State United StateAfrikaans Afrikaans
Підтримка
www.wikidata.uk-ua.nina.az

У інформатиці зокрема в представленні знань і міркуваннях і металогіці область автоматизованого міркування присвячена ро

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

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

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

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

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

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

Ранні роки

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

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

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

Значні внески

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

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

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

Системи з доведення

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

Додатки

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

Див. також

Конференції та семінари

  • [en] (IJCAR)
  • [en] (CADE)
  • [en]

Журнали

  • [en]

Спільноти

  • [en] (AAR)

Примітки

  1. Defourneaux, Gilles, and Nicolas Peltier. «Analogy and abduction in automated deduction.» IJCAI (1). 1997.
  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 . 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, . Retrieved 2010-10-10

Посилання

Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет

U informatici zokrema v predstavlenni znan i mirkuvannyah i metalogici oblast avtomatizovanogo mirkuvannya prisvyachena rozuminnyu riznih aspektiv mirkuvannya Vivchennya avtomatizovanogo mirkuvannya dopomagaye stvoryuvati komp yuterni programi yaki dozvolyayut komp yuteram mirkuvati povnistyu abo majzhe povnistyu avtomatichno Hocha avtomatizovane mirkuvannya vvazhayetsya chastinoyu sferi shtuchnogo intelektu vono takozh maye zv yazok z teoretichnoyu informatikoyu ta filosofiyeyu Najrozvinenishimi pidgaluzyami avtomatizovanogo mirkuvannya ye avtomatizovane dovedennya teorem i mensh avtomatizovana ale bilsh pragmatichna pidgaluz en i avtomatizovana perevirka dokaziv rozglyadayetsya yak garantovano pravilne mirkuvannya za fiksovanih pripushen Takozh provedena velika robota v mirkuvannyah za analogiyeyu z vikoristannyam indukciyi ta en Inshi vazhlivi temi vklyuchayut mirkuvannya v umovah neviznachenosti ta nemonotonni mirkuvannya Vazhlivoyu chastinoyu polya neviznachenosti ye argumentaciya de na dodatok do bilsh standartnogo avtomatizovanogo vivedennya zastosovuyutsya dodatkovi obmezhennya minimalnosti ta poslidovnosti Sistema OSCAR Dzhona Pollaka ye prikladom avtomatizovanoyi sistemi argumentaciyi yaka ye bilsh konkretnoyu nizh prosto avtomatizovane dovedennya teorem Instrumenti ta metodi avtomatizovanogo mirkuvannya vklyuchayut klasichnu logiku ta obchislennya nechitku logiku bajyesivskij visnovok mirkuvannya z en ta bagato mensh formalnih specialnih metodiv Ranni rokiRozvitok formalnoyi logiki vidigrav veliku rol u sferi avtomatizovanogo mirkuvannya sho samo po sobi prizvelo do rozvitku shtuchnogo intelektu Formalnij dokaz ce dovedennya u yakomu kozhen logichnij visnovok pereviryayetsya do fundamentalnih aksiom matematiki Nadayutsya vsi bez vinyatku promizhni logichni kroki Do intuyiciyi ne zvertayutsya navit yaksho pereklad z intuyiciyi na logiku ye rutinnim Takim chinom formalnij dokaz mensh intuyitivno zrozumilij i mensh shilnij do logichnih pomilok Deyaki vvazhayut sho litnya zustrich u Korneliyi 1957 roku na yakij zibralosya bagato logikiv i vchenih komp yuternikiv ye dzherelom avtomatizovanogo mirkuvannya abo avtomatizovanogo vivedennya Inshi kazhut sho ce pochalosya do cogo z programi en Nyuella en ta Sajmona 1955 roku abo z vprovadzhennyam Martinom Devisom u 1954 roci proceduri rishennya Presburgera yaka dovela sho suma dvoh parnih chisel ye parnoyu Avtomatizovani mirkuvannya hocha i ye vazhlivoyu ta populyarnoyu oblastyu doslidzhen projshli cherez zimu ShI u visimdesyatih ta na pochatku dev yanostih Odnak zgodom ce pole doslidzhen vidrodilosya Napriklad u 2005 roci Microsoft pochala vikoristovuvati tehnologiyu perevirki v bagatoh svoyih vnutrishnih proyektah i planuvala vklyuchiti logichnu specifikaciyu ta movu perevirki u svoyu versiyu Visual C 2012 roku Znachni vneskiPrincipia Mathematica bula vazhlivoyu robotoyu u formalnij logici napisanoyu Alfredom Nortom Uajthedom i Bertranom Rasselom Principia Mathematica sho takozh oznachaye Principi matematiki bula napisana z metoyu vivedennya vsih abo deyakih matematichnih viraziv u terminah simvolichnoyi logiki Principia Mathematica spochatku bula opublikovana v troh tomah u 1910 1912 ta 1913 rokah en LT bula pershoyu programoyu rozroblenoyu v 1956 roci Allenom Nyuellom en ta Gerbertom A Sajmonom shob imituvati lyudski mirkuvannya pid chas dovedennya teorem i bula prodemonstrovana na p yatdesyati dvoh teoremah z rozdilu drugoyi knigi Principia Mathematica dovodyachi tridcyat visim z nih Okrim dovedennya teorem programa znajshla dovedennya odniyeyi z teorem yakij buv bilsh elegantnim nizh toj yakij nadali Uajthed ta Rassel Pislya nevdaloyi sprobi opublikuvati svoyi rezultati Nyuell Shou ta Gerbert povidomili u svoyij publikaciyi 1958 roku Nastupnij progres u doslidzhenni operacij Zaraz u sviti ye mashini yaki dumayut vchatsya i tvoryat Shobilshe yihnya zdatnist robiti ce bude shvidko zrostati doki u vidimomu majbutnomu kolo problem z yakimi voni mozhut vporatisya ne bude odnakovo shirokim z diapazonom do yakogo buv zastosovanij lyudskij rozum dd Sistemi z dovedennyaDovidnik teoremi Bojyera Mura NQTHM Na rozrobku en vplinuli Dzhon Makkarti ta Vudi Bledso Rozpochatij u 1971 roci v Edinburzi Shotlandiya ce bula povnistyu avtomatichna sistema z dovedennya teorem stvorena za dopomogoyu Pure Lisp Osnovnimi aspektami NQTHM buli vikoristannya Lisp yak robochoyi logiki opora na princip viznachennya dlya povnih rekursivnih funkcij shiroke vikoristannya perepisuvannya ta simvolichnoyi ocinki indukcijna evristika zasnovana na nevdachi simvolichnogo ocinyuvannya HOL Light Napisanij na OCaml en rozrobleno shob mati prostu j chistu logichnu osnovu ta vilnu realizaciyu Po suti ce she odin pomichnik po dovedennyu dlya klasichnoyi logiki vishogo poryadku Coq Rozroblenij u Franciyi Coq ye she odnim avtomatizovanim pomichnikom perevirki yakij mozhe avtomatichno vityaguvati vikonuvani programi zi specifikacij u viglyadi vihidnogo kodu Objective CAML abo Haskell Vlastivosti programi ta dovedennya formalizovani tiyeyu zh movoyu sho nazivayetsya obchislennyam induktivnih konstrukcij angl Calculus of Inductive Constructions CIC DodatkiAvtomatichne mirkuvannya najchastishe vikoristovuyetsya dlya pobudovi avtomatizovanih doveden teorem Chasto odnak dlya dovedennya teorem potribni pevni vkazivki lyudini shob buti efektivnimi i tomu v bilsh zagalnomu sensi voni kvalifikuyutsya yak pomichniki dlya dovedennya U deyakih vipadkah taki dovidniki vinajshli novi pidhodi do dovedennya teoremi en ye horoshim prikladom cogo Programa znajshla dovedennya odniyeyi z teorem Principia Mathematica yakij buv efektivnishim vimagav menshe krokiv nizh dovedennya nadane Vajtgedom i Rasselom Programi dlya avtomatizovanih mirkuvan zastosovuyutsya dlya virishennya vse bilshoyi kilkosti problem z formalnoyi logiki matematiki ta informatiki logichnogo programuvannya perevirki programnogo ta aparatnogo zabezpechennya proyektuvannya shem ta bagatoh inshih TPTP Sutcliffe and Suttner 1998 ce biblioteka takih problem yaka regulyarno onovlyuyetsya Takozh na konferenciyi en regulyarno provodyatsya zmagannya sered avtomatizovanih dokaznikiv teorem Pelletier Sutcliffe and Suttner 2002 zavdannya dlya konkursu vibirayutsya z biblioteki TPTP Div takozhAvtomatichne mashinne navchannya AutoML Avtomatizovane dovedennya teoremi en en en Zastosuvannya shtuchnogo intelektu en Kazuyistika en en Mehanizm visnovku en Konferenciyi ta seminari en IJCAR en CADE en Zhurnali en Spilnoti en AAR PrimitkiDefourneaux Gilles and Nicolas Peltier Analogy and abduction in automated deduction IJCAI 1 1997 C Hales Thomas Formal Proof University of Pittsburgh Retrieved on 2010 10 19 Automated Deduction AD The Nature of PRL Project Retrieved on 2010 10 19 Martin Davis 1983 The Prehistory and Early History of Automated Deduction U Jorg Siekmann red Automation of Reasoning 1 Classical Papers on Computational Logic 1957 1966 Heidelberg Springer s 1 28 ISBN 978 3 642 81954 4 Here p 15 Principia Mathematica at Stanford University Retrieved 2010 10 19 The Logic Theorist and its Children Retrieved 2010 10 18 Shankar Natarajan Little Engines of Proof Computer Science Laboratory SRI International Retrieved 2010 10 19 The Boyer Moore Theorem Prover Retrieved on 2010 10 23 Harrison John HOL Light an overview Retrieved 2010 10 23 Introduction to Coq Retrieved 2010 10 23 Automated Reasoning Retrieved 2010 10 10Posilannya

Дата публікації:
Топ