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. ^[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

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

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

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. ^[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

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

↑ 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
↑ ^a ^b "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

Datuak: Q2555318

[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

[cornell-4] "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

[Shankar1994-8] ISBN 9780521585330..

[Russinoff1992-9] :10.1007/BF00263446..

[Gonthier2013-10] :10.1007/978-3-642-39634-2_14. ISBN 978-3-642-39633-5..

[Heule2016-11] :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

[Stanford_Encyclopedia-15] Automated Reasoning, Stanford Encyclopedia. Retrieved 2010-10-10

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]