Wikipedia

Arrazoiketa automatiko

(«Arrazoiketa automatikoa» orritik birbideratua)

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. [1]

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[2] 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 aldatu

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.[3]

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

Ekarpen garrantzitsuak aldatu

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.₤[5]

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. [6] 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." [7]

Froga formalen adibideak

Urtea Teorema Frogatzailea Formalizatzailea Ohiko froga
1986 First Incompleteness Boyer-Moore Shankar[8] Gödel
1990 Quadratic Reciprocity Boyer-Moore Russinoff[9] 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.[10] Bender, Glauberman and Peterfalvi
2016 Boolean Pythagorean triples problem Formalized as SAT Heule et al.[11] None

Froga-sistemak aldatu

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:
  1. Lisp erabiltzea lan-logika gisa.
  2. funtzio erabat errekurtsiboen definizio-printzipio batean oinarritzea.
  3. berridazketaren eta "ebaluazio sinbolikoaren" erabilera zabala .
  4. ebaluazio sinbolikoaren porrotaren oinarria ematen zuen indukzio-heuristiko batek. [12]
HOL Light
OCaml lengoaiaz idatzita, HOL Light oinarri logiko soil eta garbia izateko diseinatuta dago. Funtsean, goi mailako logika klasikorako beste froga-laguntzailea da. [13]
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. [14]

Aplikazioak aldatu

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. [15]

Erreferentziak aldatu

  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. ↑ a b "Automated Deduction (AD)", [The Nature of PRL Project]. Retrieved on 2010-10-19
  5. ↑ "Principia Mathematica", at Stanford University. Retrieved 2010-10-19
  6. ↑ "The Logic Theorist and its Children". Retrieved 2010-10-18
  7. ↑ Shankar, Natarajan Little Engines of Proof, Computer Science Laboratory, SRI International. Retrieved 2010-10-19
  8. ↑ ISBN 9780521585330..
  9. ↑  doi:10.1007/BF00263446..
  10. ↑  doi:10.1007/978-3-642-39634-2_14. ISBN 978-3-642-39633-5..
  11. ↑  doi:10.1007/978-3-319-40970-2_15. ISBN 978-3-319-40969-6..
  12. ↑ The Boyer- Moore Theorem Prover. Retrieved on 2010-10-23
  13. ↑ Harrison, John HOL Light: an overview. Retrieved 2010-10-23
  14. ↑ Introduction to Coq. Retrieved 2010-10-23
  15. ↑ Automated Reasoning, Stanford Encyclopedia. Retrieved 2010-10-10

Ikus, gainera aldatu

  • 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 aldatu

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

Aldizkariak aldatu

  • Journal of Automated Reasoning

Komunitateak aldatu

  • Arrazoibide Automatikorako Elkartea (AAR)

Kanpo estekak aldatu

"https://eu.wikipedia.org/w/index.php?title=Arrazoiketa_automatiko&oldid=8568488"(e)tik eskuratuta