Arrazoiketa automatiko

Arrazoiketa automatikoa (edo arrazoibide automatikoa) informatikaren eremu bat ezagutzaren errepresentazioa eta arrazoibideak) eta metalogika eremuak bere barruan darabiltzana, eta arrazoitzeko moduak ulertzeko hainbat alderdi lantzen dituena. Arrazoibide automatizatuaren azterketak arrazoitzea ahalbidetzen duten programa informatikoak sortzen laguntzen du, erabat edo ia erabat automatikoki. Arrazoibide automatizatuak adimen artifizialaren azpi-eremutzat jotzen diren arren, informatika teorikoarekin eta filosofiarekin ere baditu loturak.

Arrazoibide automatizatuen azpieremu garatuenak teoremen frogapen automatikoa (eta hain automatikoa ez den baina pragmatikoa den teoremen frogapen interaktiboa azpieremua) eta egiaztapen automatizatua (hipotesi finkoen pean arrazoibide zuzen bermatu gisa ikusten dena).  Analogia bidez Indukzio eta abdukzioa erabiliz ere lan handia egin da arrazoibidean. Defourneaux, Gilles, and Nicolas Peltier. "Analogy and abduction in automated deduction." IJCAI (1). 1997.

Beste gai garrantzitsuen artean ziurgabetasunaren arrazoibidea eta arrazonamendu ez monotonikoa dira aipagarri. Ziurgabetasunaren eremuko zati garrantzitsu bat argumentazioarena da, non gutxieneko eta koherentziazko muga gehiago aplikatzen diren dedukzio automatizatu estandarragoaren gainean. John Pollock-en OSCAR sistemaJohn L. Pollock teorema-frogapen automatiko bat baino zehatzagoa den argumentazio-sistema automatizatuaren adibidea da.

Arrazoibide automatizatuaren tresna eta teknika batzuk dira honako hauek: logika eta kalkulu klasikoak, logika lausoa, inferentzia bayesiarra, entropia maximoa duten arrazoibideak eta hain formalak ez diren ad hoc teknikak.

 Hasierako urteak 
Logika formalaren garapenak zeresan handia izan zuen arrazoibide automatizatuaren arloan, eta horrek berak ekarri zuen adimen artifiziala garatzea. Froga formal batean inferentzia logikoa eta matematikaren oinarrizko axiomak erabiltzen dira. Tarteko urrats logiko guzti-guztiak ematen dira, salbuespenik gabe. Intuizioari ez da erabiltzen, nahiz eta intuiziotik logikara pasatzea ohikoa izaten den. Beraz, froga formal bat ez da hain intuitiboa eta akats logiko gutxiago jasaten ohi ditu.C. Hales, Thomas "Formal Proof", University of Pittsburgh. Retrieved on 2010-10-19

Batzuek 1957ko Cornell Summer bilera, logikari eta informatikari ugari bildu zituen arrazoibide automatizatuaren edo teoremen frogapen automatizatuaren jatorritzat jotzen dute."Automated Deduction (AD)", [The Nature of PRL Project]. Retrieved on 2010-10-19 Beste batzuek diote aurretik hasi zela Newell, Shaw eta Simon-en 1955eko Logic Theorist programarekin edo Martin Davis-ek 1954an Presburger-en erabaki-prozedura gauzatu zuenean (frogatu zuen bi zenbaki bikoitiren batura bikoitia dela).

Arrazoibide automatizatuak, nahiz eta ikerketa-arlo esanguratsu eta ezaguna izan, "Adimen Artifizialaren negua" igaro zuen laurogeiko eta laurogeita hamarreko hamarkadetan. Eremua berpiztu egin zen, ordea. Adibidez, 2005ean, Microsoft egiaztapen-teknologia erabiltzen hasi zen barne proiektu askotan eta zehaztapen logikoa eta egiaztapen-lengoaia bat sartu zuen 2012ko Visual C bertsioan."Automated Deduction (AD)", [The Nature of PRL Project]. Retrieved on 2010-10-19

 Ekarpen garrantzitsuak 
Principia Mathematica Alfred North Whitehead-ek eta Bertrand Russell-ek idatzitako logika formalaren mugarri bat izan zen. Principia Mathematica ―Matematikaren printzipioak ere esan nahi duena― adierazpen matematiko guztiak edo batzuk logika sinbolikoaren arabera eratortzeko idatzi zen. Principia Mathematica hiru liburukitan argitaratu zen hasiera batean 1910, 1912 eta 1913. urteetan.₤"Principia Mathematica", at Stanford University. Retrieved 2010-10-19

Logic Theorist (LT) Allen Newellek, Cliff Shaw-ek eta Herbert A. Simon-ek 1956an garatu zuten lehen programa izan zen, teoremak frogatzeko "giza arrazoibidea imitatzen" zuena ; Principia Mathematica-ko bigarren kapituluko berrogeita hamabi teoremekin saiatu ziren, eta horietako hogeita hamazortzi frogatu zituzten. "The Logic Theorist and its Children". Retrieved 2010-10-18 Programak teoremak frogatzeaz gain, Whitehead-ek eta Russell-ek emandakoa baino dotoreagoa zen teorema-froga bat aurkitu zuen. Emaitzak argitaratzeko saiakera arrakastatsua egin ondoren, Newell-ek, Shaw-ek eta Herbert-ek 1958an argitaratu zuten The Next Advance in Operation Research :

 "Badira munduan pentsatzen, ikasten eta sortzen duten makinak. Are gehiago, horrelakoak egiteko duten gaitasuna bizkor handituko da (etorkizun ikusgarri batean) lan dezaketen arazoen eremua gizakiaren adimena aplikagarri den barruti osora hedatu arte." Shankar, Natarajan Little Engines of Proof, Computer Science Laboratory, SRI International. Retrieved 2010-10-19

Froga formalen adibideak
{| class="wikitable"
|-
! Urtea !! Teorema !! Frogatzailea !! Formalizatzailea !! Ohiko froga
|-
| 1986 || First Incompleteness|| Boyer-Moore || Shankar || Gödel
|-
| 1990 || Quadratic Reciprocity || Boyer-Moore || Russinoff || Eisenstein
|-
| 1996 || Fundamental- of Calculus || HOL Light || Harrison || Henstock
|-
| 2000 || Fundamental- of Algebra || Mizar || Milewski || Brynski
|-
| 2000 || Fundamental- of Algebra || Coq || Geuvers et al. || Kneser
|-
| 2004 || Four Color || Coq || Gonthier || Robertson et al.
|-
| 2004 || Prime Number || Isabelle || Avigad et al. || Selberg-Erdős
|-
| 2005 || Jordan Curve || HOL Light || Hales || Thomassen
|-
| 2005 || Brouwer Fixed Point || HOL Light || Harrison || Kuhn
|-
| 2006 || Flyspeck 1 || Isabelle || Bauer- Nipkow || Hales
|-
| 2007 || Cauchy Residue || HOL Light || Harrison || Classical
|-
| 2008 || Prime Number || HOL Light || Harrison || Analytic proof
|-
| 2012 || Feit-Thompson || Coq || Gonthier et al. || Bender, Glauberman and Peterfalvi
|-
| 2016 || Boolean Pythagorean triples problem || Formalized as SAT || Heule et al. || None
|}
 Froga-sistemak 

 Boyer-Moore Teorema-frogatzailea (NQTHM)
 NQTHM sistemaren diseinuak John McCarthy eta Woody Bledsoe-ren eragina izan zuen. 1971an hasi zen Edinburgh-en, Eskozian, Pure Lisp erabiliz eraikitako teorema-frogatzaile guztiz automatikoa. NQTHMren alderdi nagusiak hauek izan ziren:
 Lisp erabiltzea lan-logika gisa.
 funtzio erabat errekurtsiboen definizio-printzipio batean oinarritzea.
 berridazketaren eta "ebaluazio sinbolikoaren" erabilera zabala .
 ebaluazio sinbolikoaren porrotaren oinarria ematen zuen indukzio-heuristiko batek. The Boyer- Moore Theorem Prover. Retrieved on 2010-10-23

 HOL Light
 OCaml lengoaiaz idatzita, HOL Light oinarri logiko soil eta garbia izateko diseinatuta dago. Funtsean, goi mailako logika klasikorako beste froga-laguntzailea da. Harrison, John HOL Light: an overview. Retrieved 2010-10-23

 Coq
 Frantzian garatua, Coq beste froga-laguntzaile automatizatu bat da, programa exekutagarriak automatikoki atera ditzake zehaztapenetatik, baita Objective CAML edo Haskell iturburu-kodea ere. Propietateak, programak eta frogapenak Eraikuntza Induktiboen Kalkulua (CIC, Calculus of Inductive Constructions) izeneko lengoaia berean formalizatzen dira. Introduction to Coq. Retrieved 2010-10-23

 Aplikazioak 
Arrazoibide automatizatua teorema-frogatzaile automatizatuak eraikitzeko erabili da gehienbat. Askotan, ordea, teorema-frogatzaileek giza orientazioa behar dute eraginkorra izateko eta, beraz, orokorrean froga laguntzaile gisa kalifikatzen dira. Zenbait kasutan, horrelako frogatzaileek teorema bat frogatzeko ikuspegi berriak planteatu dituzte. Logic Theorist da horren adibide ona. Principia Mathematica-ko teoremetako baten frogak sortu zituen programak Whitehead-ek eta Russell-ek emandako froga bat baino eraginkorragoa zen (urrats gutxiago behar izan zituen).

Arrazonamendu-programa automatizatuak aplikatzen ari dira hainbat alorretako arazoak konpontzeko: logika formalean, matematikan eta informatikan, programazio logikoan, software eta hardwarearen egiaztapenean, zirkuituen diseinuan eta beste askotan. TPTP liburutegia (Sutcliffe eta Suttner 1998) horrelako problema lantzen ditu, eta aldian-aldian eguneratzen dute. CADE konferentzian lehiaketa bat ere badago aldizka antolatzen dena teorema-frogatzaile automatikoen artean (Pelletier, Sutcliffe eta Suttner 2002) ; lehiaketarako problemak TPTP liburutegitik hautatzen dira. Automated Reasoning, Stanford Encyclopedia. Retrieved 2010-10-10

 Erreferentziak 

 Ikus, gainera 

 Ikasketa automatiko automatikoa (AutoML)
 Teoremen egiaztapen automatizatua
 Arrazoibide sistema
 Arrazoibide semantikoa
 Programen analisia (informatika)
 Adimen artifizialaren aplikazioak
 Adimen artifizialaren eskema
 Kasuistika • Kasuetan oinarritutako arrazoibidea
 Abdukziozko arrazoibidea
 Inferentzia motorra
 Commonsense arrazoibidea

 Jardunaldiak eta tailerrak 

 Arrazoibide automatizatuari buruzko nazioarteko konferentzia bateratua (IJCAR)
 Dedukzio automatikoari buruzko konferentzia (CADE)
 Arrazoibide automatizatuari buruzko nazioarteko konferentzia, taula analitikoekin eta erlazionatutako metodoekin

 Aldizkariak 

 Journal of Automated Reasoning

 Komunitateak 

 Arrazoibide Automatikorako Elkartea (AAR)

 Kanpo estekak 

 Logikak ezartzeko nazioarteko tailerra
 Arrazonamendu automatizatuan enpirikoki arrakastatsuak diren gaiei buruzko tailerrak

Kategoria:Adimen artifiziala
Kategoria:Informatika teorikoa