Raonament automàtic
El raonament automatizado és un pancho de la ciències de la computació dedicada a comprendre diferents aspectes del raonament de manera que permeta la creació de programes informàtics que possibiliten als ordenadors raonar de forma completament automàtica, o casi automàtica. Se li considera habitualment com una subárea de l'inteligència artificial, pero ademés posseïx fortes conexions en la Teoria de la computació i inclús en la filosofia.
Història
[editar | editar còdic]L'història del raonament automatizado es remonta als primers indicis de la mecanisació del mateix, que poden remontar-se a la filosofia de l'Antiga Grècia, que va donar orige, finalment de la mà d'Aristóteles, al tractat de llògica proposicional descrit en la seua compendio de llibres, Órganon. Este pretenia esquematizar els raonaments usant símbols que sustitutían a les distintes afirmacions (proposicions) que formaven part d'un raonament. Els debats i discussions sobre llògica proposicional varen estar des de llavors en voga dels filòsofs grecs, fins a l'arribada de l'Edat Mija. Per eixemple, i sobre l'interpretació de la conectiva cridada implicador, Calímaco va aplegar a dir:
En l'arribada dels pobles bàrbars, i la caiguda de la cultura clàssica, l'Europa Medieval va perdre i no va revivar l'interés científic aproximadament fins al sigle XII en l'introducció dels texts aristotèlics, que des de llavors varen governar la filosofia escolàstica, al voltant del sigle XI, duts i recopilats celosament des de feya sigles per la tradició musulmana, en la Casa del saber.
Açò va propiciar l'aparició de la cridada Revolució Científica del sigle XII, que va tornar a revivar, entre atres coses, les preocupacions de la llògica, encara des d'un punt de vista totalment filosòfic.
Ya en el 1305, el pensador català Ramon Llull, fortament influenciat per Roger Bacon (un dels primers revolucionaris del sigle XII), va escriure un tractat, el Ars Magna, que pot considerar-se un clar precursor del raonament automatizado, ya entés com un procediment mecànic que raona per sí mateixa. A diferència de la llògica aristotèlica (sinònima de proposicional), que solament és una ferramenta per a fer raonaments des d'un punt de vista més analític, pero realisats en última instància per l'individu, el Ars Magna de Llull era un sistema de circumferències en etiquetes de símbols que representen conceptes, i que conectats com si d'una maquinària de rellonge es tractara, permetia seleccionar distints atributs o conceptes en la màquina, i, accionándola, permetria aplegar a les conclusions de dit raonament. Estos estaven molt fortament imbuidos de conceptes teològics i filosòfics, per a realisar raonaments en estes àrees, de modo que s'aplegara a veritats indiscutibles (de principal orientació a l'ideologia cristiana), a partir de conceptes que atribuirien com a verdaders tant judeus com a musulmans, a fi de convéncer a abdós bandos.
El següent esclavó d'esta cadena recaïa en possessió de Gottfried Leibniz. Per la seua forta convicció racionaliste, va reflexionar sobre la possibilitat de construir, ya no solament una màquina, sino també un llenguage universal (concepte preconisat per René Descartes, pare del racionalisme) que tinguera el suficient poder d'expressió per a raonar en coherència, rigidea i sense ambigüitat sobre qualsevol tipo de concepte. Ell es va inspirar en el Ars Magna de Llull per a construir este Ars combinatòria.
Durant tot este periodo, l'estudi sobre el raonament, tant mecànic com a analític, caïa dins del camp de la filosofia i en les mans dels filòsofs i matemàtics en inclinaments filosòfics.
Va ser en el sigle XIX i XX, ya de la mà de la matemàtica, a on es varen obtindre nous enfocaments sobre el raonament. El principal interés va ser axiomatizar la matemàtica en una teoria axiomàtica basal que la constituïra sancera, entre els principals autors de la qual i responsables poden citar-se a Dedekind (que va conseguir reunir la matemàtica numèrica i infinitesimal, per mig de les cridades cortaduras de Dedekind), els debats i la disputa entre Georg Cantor, Gottlob Frege i Bertrand Russell (sobre els problemes i conceptes de l'infinit i el conjunt, i la construcció de la llògica de primer orde), David Hilbert, establint el seu finitismo metodològic, i per últim Ernst Zermelo i Adolf Fraenkel que varen construir el seu axiomàtica ZF, que ha permaneixcut pràcticament invariable fins als nostres dies. Es va conseguir llavors culminar este procés de axiomatisació que la matemàtica duya experimentant durant més d'un sigle.
I és este procés el que va propiciar els nous enfocaments sobre el raonament automatizado modern. Una volta conseguit un marc formal de raonament i construcció de la matemàtica, la següent pregunta òbvia era la capacitat mecànica dels sistemes que s'acaben de constituir. És dir, quina informació m'otorguen els símbols, quines conexions poden existir entre les premisses i les conclusions que s'intenten demostrar, dins d'una teoria axiomàtica, i quins són les seues llimitacions teòriques. Dit d'una atra forma, fins a quin punt un matemàtic o un llògic podia traslladar als símbols la responsabilitat de realisar l'horrible i tediós treball de conseguir demostrar teoremes, en solament seguir els passos marcats per un procediment mecànic.
Les respostes a estes preguntes varen tindre dos eixides principals: la primera va ser la construcció de tot el corpus matemàtic de la computació (la formalisació del concepte d'algoritme, és dir, la formalisació del concepte de procés mecànic i funció computable), principalment de la mà d'Alan Turing, i la segona els resultats sobre les llimitacions d'expressió i aptitut dels llenguages formals, que són els usats per a raonar, resultats principalment presos de la mà de Kurt Gödel.
A partir de tots estos resultats teòrics conjunts, va escomençar a divergir la seua utilitat pràctica (a lo manco en els problemes que caben dins de les llimitacions teòriques), en la construcció de softwares de raonament, tant automatizado com interactiu, per a ajudar, per eixemple, a guiar a l'usuari que desige demostrar algunes teoremes dels seus propis sistemes, per eixemple, en problemes de verificació del software.
Subárea
[editar | editar còdic]Les subárea més desenrollades del raonament automatizado són provablement la demostració automàtica de teoremes (i la menys automàtica, pero més pragmàtica demostració interactiva de teoremes i la verificació de demostracions (que garantisa que un raonament és correcte). Ademés, s'ha realisat un treball enorme en el raonament per analogia, inducció i abducció. Atres temes importants són el raonament en incertitut i el raonament no monòton. Una part important del raonament en incertitut és l'argumentació, a on s'apliquen restriccions de minimalidad i de consistència sobre el raonament automatizado clàssic. El sistema Oscar de John Pollock és un eixemple d'argumentació automàtica que és més específic que un "simple" demostrador automatizado de teoremes. L'argumentació formal és un subárea de l'inteligència artificial.
Les ferramentes i les tècniques del raonament automatizado inclouen les llògiques i els càlculs clàssics de demostració automàtica de teoremes, aixina com la llògica difusa, l'inferència bayesiana el raonament pel principi d'entropía maximal i un gran número de tècniques ad hoc menys formals.
Referències
[editar | editar còdic]- Este artícul conté una traducció derivada de «Automated reasoning» de Wikipedia en inglés publicada baix la Llicència de documentació lliure de GNU i la Llicència Creative Commons Reconeiximent-CompartirIgual 4.0 Internacional.
- Este artícul conté una traducció derivada de «Raisonnement automatisé» de Wikipedia en francés publicada baix la Llicència de documentació lliure de GNU i la Llicència Creative Commons Reconeiximent-CompartirIgual 4.0 Internacional.
- Portoraro, Frederic Automated Reasoning. The Stanford Encyclopedia of Philosophy (Winter 2008 Edition), Edward N. Zalta (ed.).