# 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.
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 sistema 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.
Batzuek 1957ko Cornell Summer bilera, logikari eta informatikari ugari bildu zituen arrazoibide automatizatuaren edo teoremen frogapen automatizatuaren jatorritzat jotzen dute. 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.

## 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.₤
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. 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."
Froga formalen adibideak
    UrteaTeoremaFrogatzaileaFormalizatzaileaOhiko froga 1986First IncompletenessBoyer-MooreShankarGödel 1990Quadratic ReciprocityBoyer-MooreRussinoffEisenstein 1996Fundamental- of CalculusHOL LightHarrisonHenstock 2000Fundamental- of AlgebraMizarMilewskiBrynski 2000Fundamental- of AlgebraCoqGeuvers et al.Kneser 2004Four ColorCoqGonthierRobertson et al. 2004Prime NumberIsabelleAvigad et al.Selberg-Erdős 2005Jordan CurveHOL LightHalesThomassen 2005Brouwer Fixed PointHOL LightHarrisonKuhn 2006Flyspeck 1IsabelleBauer- NipkowHales 2007Cauchy ResidueHOL LightHarrisonClassical 2008Prime NumberHOL LightHarrisonAnalytic proof 2012Feit-ThompsonCoqGonthier et al.Bender, Glauberman and Peterfalvi 2016Boolean Pythagorean triples problemFormalized as SATHeule 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.

### HOL Light

    OCaml lengoaiaz idatzita, HOL Light oinarri logiko soil eta garbia izateko diseinatuta dago. Funtsean, goi mailako logika klasikorako beste froga-laguntzailea da.

### 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.

## 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.

## Erreferentziak

* ↑ Defourneaux, Gilles, and Nicolas Peltier. "Analogy and abduction in automated deduction." IJCAI (1). 1997.
* ↑ John L. Pollock
* ↑ C. Hales, Thomas "Formal Proof", University of Pittsburgh. Retrieved on 2010-10-19
* 1 2 "Automated Deduction (AD)", [The Nature of PRL Project]. Retrieved on 2010-10-19
* ↑ "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
* ↑ ISBN 9780521585330..
* ↑ doi:10.1007/BF00263446..
* ↑ doi:10.1007/978-3-642-39634-2_14. ISBN 978-3-642-39633-5..
* ↑ doi:10.1007/978-3-319-40970-2_15. ISBN 978-3-319-40969-6..
* ↑ 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, Stanford Encyclopedia. Retrieved 2010-10-10

## 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
* Datuak: Q2555318