Automatické uvažování - Automated reasoning

Automatické uvažování je oblast počítačová věda (zahrnuje reprezentace znalostí a uvažování ) a metalogický věnovaný porozumění různým aspektům uvažování. Studie automatizovaného uvažování pomáhá produkovat počítačové programy které počítačům umožňují zcela nebo téměř úplně automaticky uvažovat. Ačkoli automatické uvažování je považováno za dílčí pole umělá inteligence, má také spojení s teoretická informatika, a dokonce filozofie.

Nejrozvinutější podoblasti automatizovaného uvažování jsou automatizované dokazování věty (a méně automatizované, ale pragmatičtější podpole z interaktivní dokazování věty ) a automatická kontrola kontroly (považováno za zaručené správné uvažování za pevných předpokladů).[Citace je zapotřebí ] Rozsáhlá práce byla také provedena v úvahách od analogie použitím indukce a únos.[1]

Mezi další důležitá témata patří uvažování pod nejistota a nemonotónní uvažování. Důležitou součástí pole nejistoty je pole argumentace, kde se na standardnější automatizovaný odpočet aplikují další omezení minimality a konzistence. Systém OSCAR Johna Pollocka[2] je příkladem automatizovaného argumentačního systému, který je konkrétnější, než být jen automatizovaným testerem vět.

Mezi nástroje a techniky automatizovaného uvažování patří klasická logika a kalkul, fuzzy logika, Bayesovský závěr, uvažování s maximální entropie a mnoho méně formálních ad hoc techniky.

Raná léta

Vývoj formální logika hrála velkou roli v oblasti automatizovaného uvažování, což samo o sobě vedlo k rozvoji umělá inteligence. A formální důkaz je důkaz, ve kterém byly všechny logické závěry zkontrolovány zpět na základní axiomy matematiky. Všechny mezilehlé logické kroky jsou dodávány bez výjimky. Intuice není nijak lákavá, i když je překlad z intuice do logiky rutinní. Formální důkaz je tedy méně intuitivní a méně náchylný k logickým chybám.[3]

Někteří považují za počátek automatického uvažování setkání Cornellova léta z roku 1957, které spojilo mnoho logiků a počítačových vědců, nebo automatický odpočet.[4] Jiní říkají, že to začalo předtím 1955 Logický teoretik program Newell, Shaw a Simon, nebo implementace Martin Davis z roku 1954 Postup rozhodování Presburgera (což dokázalo, že součet dvou sudých čísel je sudý).[5]

Automatické uvažování, přestože je významnou a populární oblastí výzkumu, prošlo „AI zima „v osmdesátých a na počátku devadesátých let. Pole se však následně oživilo. Například v roce 2005 Microsoft začal používat ověřovací technologie v mnoha svých interních projektech a plánuje zahrnout logickou specifikaci a kontrolní jazyk do své verze Visual C. 2012.[4]

Významné příspěvky

Principia Mathematica byla mezníkem v roce formální logika napsáno Alfred North Whitehead a Bertrand Russell. Principia Mathematica - také význam Principy matematiky - byl napsán s cílem odvodit všechny nebo některé z matematické výrazy, ve smyslu symbolická logika. Principia Mathematica byla původně vydána ve třech svazcích v letech 1910, 1912 a 1913.[6]

Logický teoretik (LT) byl vůbec prvním programem vyvinutým v roce 1956 společností Allen Newell, Cliff Shaw a Herbert A. Simon „napodobovat lidské uvažování“ při dokazování vět a bylo prokázáno na padesáti dvou větách z druhé kapitoly Principia Mathematica, z nichž bylo prokázáno třicet osm.[7] Kromě prokázání vět, program našel důkaz pro jednu z vět, který byl elegantnější než ten, který poskytli Whitehead a Russell. Po neúspěšném pokusu o zveřejnění jejich výsledků Newell, Shaw a Herbert uvedli ve své publikaci v roce 1958, Další pokrok v operačním výzkumu:

„Na světě nyní existují stroje, které myslí, učí se a vytvářejí. Navíc jejich schopnost dělat tyto věci se bude rychle zvyšovat, dokud (ve viditelné budoucnosti) nebude rozsah problémů, se kterými se mohou vyrovnat, souběžný rozsah, na který byla lidská mysl aplikována. “[8]

Příklady formálních důkazů

RokTeorémDůkazní systémFormalizátorTradiční důkaz
1986První neúplnostBoyer-MooreShankar[9]Gödel
1990Kvadratická vzájemnostBoyer-MooreRussinoff[10]Eisenstein
1996Základní - kalkuluHOL LightHarrisonHenstock
2000Základní - algebryMizarMilewskiBrynski
2000Základní - algebryCoqGeuvers et al.Kneser
2004Čtyři barvyCoqGonthierRobertson et al.
2004PrvočísloIsabelleAvigad a kol.Selberg -Erdős
2005Jordan CurveHOL LightHalesThomassen
2005Pevný bod BrouweraHOL LightHarrisonKuhn
2006Flyspeck 1IsabelleBauer - NipkowHales
2007Cauchyho reziduumHOL LightHarrisonKlasický
2008PrvočísloHOL LightHarrisonAnalytický důkaz
2012Feit-ThompsonCoqGonthier a kol.[11]Bender, Glauberman a Peterfalvi
2016Booleovský Pythagorejský problém ztrojnásobujeFormalizováno jako SATHeule a kol.[12]Žádný

Důkazní systémy

Poskytovatel věty Boyer-Moore (NQTHM)
Návrh NQTHM byl ovlivněn Johnem McCarthym a Woodym Bledsoe. Byla zahájena v roce 1971 v Edinburghu ve Skotsku a jednalo se o plně automatický tester vět vytvořený pomocí Pure Lisp. Hlavní aspekty NQTHM byly:
  1. použití Lispu jako pracovní logiky.
  2. spoléhání se na princip definice pro úplné rekurzivní funkce.
  3. rozsáhlé používání přepisování a „symbolického hodnocení“.
  4. indukční heuristika založená na selhání symbolického vyhodnocení.[13]
HOL Light
Napsáno OCaml, HOL Light je navržen tak, aby měl jednoduchý a čistý logický základ a přehlednou implementaci. Je to v zásadě další asistent kontroly pro klasickou logiku vyššího řádu.[14]
Coq
Vyvinuto ve Francii, Coq je další automatizovaný asistent kontroly, který může automaticky extrahovat spustitelné programy ze specifikací, buď jako Objective CAML nebo Haskell zdrojový kód. Vlastnosti, programy a důkazy jsou formalizovány ve stejném jazyce, který se nazývá Calculus of Inductive Constructions (CIC).[15]

Aplikace

Automatizované uvažování se nejčastěji používá k vytváření automatizovaných testerů vět. Často však dokazující věty vyžadují, aby bylo účinné nějaké lidské vedení, a tak obecněji splňovat podmínky jako důkazní asistenti. V některých případech takoví dokazovatelé přišli s novými přístupy k prokázání věty. Logický teoretik je toho dobrým příkladem. Program přišel s důkazem pro jednu z vět v Principia Mathematica to bylo efektivnější (vyžadující méně kroků) než důkaz poskytnutý Whiteheadem a Russellem. Programy automatického uvažování se používají k řešení rostoucího počtu problémů ve formální logice, matematice a informatice, logické programování, ověření softwaru a hardwaru, návrh obvodu, a mnoho dalších. The TPTP (Sutcliffe a Suttner 1998) je knihovna takových problémů, která je pravidelně aktualizována. Existuje také soutěž mezi automatizovanými větami, které se pravidelně konají na internetu CADE konference (Pelletier, Sutcliffe a Suttner 2002); problémy soutěže jsou vybrány z knihovny TPTP.[16]

Viz také

Konference a workshopy

Časopisy

Společenství

Reference

  1. ^ Defourneaux, Gilles a Nicolas Peltier. "Analogie a únos v automatickém odečtu "IJCAI (1). 1997.
  2. ^ John L. Pollock
  3. ^ C. Hales, Thomas „Formální důkaz“, University of Pittsburgh. Citováno 2010-10-19
  4. ^ A b „Automated Deduction (AD)“, [Povaha projektu PRL]. Citováno 2010-10-19
  5. ^ Martin Davis (1983). "Pravěk a raná historie automatizovaného odpočtu". V Jörg Siekmann; G. Wrightson (eds.). Automatizace uvažování (1) - Klasické referáty o výpočetní logice 1957–1966. Heidelberg: Springer. s. 1–28. ISBN  978-3-642-81954-4. Zde: str.15
  6. ^ „Principia Mathematica“, na Stanfordská Univerzita. Citováno 2010-10-19
  7. ^ „Logický teoretik a jeho děti“. Citováno 2010-10-18
  8. ^ Shankar, Natarajan Malé motory důkazu, Laboratoř výpočetní techniky, SRI International. Citováno 2010-10-19
  9. ^ Shankar, N. (1994), Metamathematics, Machines, and Gödel's Proof, Cambridge, Velká Británie: Cambridge University Press, ISBN  9780521585330
  10. ^ Russinoff, David M. (1992), „Mechanický důkaz kvadratické vzájemnosti“, J. Autom. Důvod., 8 (1): 3–21, doi:10.1007 / BF00263446
  11. ^ Gonthier, G .; et al. (2013), „Strojově ověřený důkaz věty o zvláštním řádu“ (PDF), Blazy, S .; Paulin-Mohring, C .; Pichardie, D. (eds.), Interaktivní dokazování věty, Přednášky v informatice, 7998, str. 163–179, doi:10.1007/978-3-642-39634-2_14, ISBN  978-3-642-39633-5
  12. ^ Heule, Marijn J. H .; Kullmann, Oliver; Marek, Victor W. (2016). "Řešení a ověření booleovských Pythagorejců ztrojnásobuje problém pomocí Cube-and-Conquer". Teorie a aplikace testování uspokojivosti - SAT 2016. Přednášky z informatiky. 9710. str. 228–245. arXiv:1605.00723. doi:10.1007/978-3-319-40970-2_15. ISBN  978-3-319-40969-6.
  13. ^ Poskytovatel věty Boyer-Moore. Citováno 2010-10-23
  14. ^ Harrison, John HOL Light: přehled. Citováno 2010-10-23
  15. ^ Úvod do Coq. Citováno 2010-10-23
  16. ^ Automatizované uvažování, Stanfordská encyklopedie. Citováno 2010-10-10

externí odkazy