Raonament automatitzat

En informàtica, en particular en la representació del coneixement i el raonament i la metalògica, l'àrea del raonament automatitzat es dedica a comprendre diferents aspectes del raonament. L'estudi del raonament automatitzat ajuda a produir programes informàtics que permeten als ordinadors raonar completament, o gairebé completament, automàticament. Tot i que el raonament automatitzat es considera un subcamp de la intel·ligència artificial, també té connexions amb la informàtica teòrica i la filosofia.

Les subàrees més desenvolupades del raonament automatitzat són la demostració automatitzada de teoremes (i el subcamp menys automatitzat però més pragmàtic de la demostració interactiva de teoremes) i la verificació de proves automatitzada (vist com un raonament correcte garantit sota supòsits fixos). També s'ha fet un treball extens en el raonament per analogia utilitzant inducció i abducció.

Altres temes importants inclouen el raonament sota incertesa i el raonament no monòton. Una part important del camp d'incertesa és el de l'argumentació, on s'apliquen més restriccions de minimalitat i consistència a la deducció automatitzada més estàndard. El sistema OSCAR de John Pollock és un exemple de sistema d'argumentació automatitzat que és més específic que només un demostrador de teoremes automatitzat.

Les eines i tècniques de raonament automatitzat inclouen la lògica clàssica i els càlculs, la lògica difusa, la inferència bayesiana, el raonament amb entropia màxima i moltes tècniques ad hoc menys formals.

Primers anys

El desenvolupament de la lògica formal va tenir un paper important en el camp del raonament automatitzat, que va conduir al desenvolupament de la intel·ligència artificial. Una demostració formal és una demostració en què totes les inferències lògiques s'han comprovat als axiomes fonamentals de les matemàtiques. Es proporcionen tots els passos lògics intermedis, sense excepció. No s'apel·la a la intuïció, encara que la traducció de la intuïció a la lògica sigui rutinària. Així, una prova formal és menys intuïtiva i menys susceptible a errors lògics.

Alguns consideren la reunió d'estiu de Cornell de 1957, que va reunir molts lògics i informàtics, com l'origen del raonament automatitzat o deducció automatitzada. Altres diuen que va començar abans amb el programa de 1955 Logic Theorist de Newell, Shaw i Simon, o amb la implementació de Martin Davis de 1954 del procediment de decisió de Presburger (que va demostrar que la suma de dos nombres parells és parell).

El raonament automatitzat, tot i que una àrea de recerca important i popular, va passar per un " hivern d'IA " als anys vuitanta i principis dels noranta. El camp es va revifar posteriorment, però. Per exemple, l'any 2005, Microsoft va començar a utilitzar la tecnologia de verificació en molts dels seus projectes interns i té previst incloure una especificació lògica i un llenguatge de verificació a la seva versió de 2012 de Visual C.

Aportacions significatives

Principia Mathematica va ser una obra fita en lògica formal escrita per Alfred North Whitehead i Bertrand Russell. Principia Mathematica - també que significa Principis de Matemàtiques - va ser escrit amb el propòsit de derivar totes o algunes de les expressions matemàtiques, en termes de lògica simbòlica. Principia Mathematica es va publicar inicialment en tres volums el 1910, 1912 i 1913.

Logic Theorist (LT) va ser el primer programa desenvolupat l'any 1956 per Allen Newell, Cliff Shaw i Herbert A. Simon per "imitar el raonament humà" en la demostració de teoremes i es va demostrar amb cinquanta-dos teoremes del capítol dos de Principia Mathematica, demostrant trenta. -vuit d'ells. A més de demostrar els teoremes, el programa va trobar una demostració per a un dels teoremes que era més elegant que la proporcionada per Whitehead i Russell. Després d'un intent infructuós de publicar els seus resultats, Newell, Shaw i Herbert van informar a la seva publicació el 1958, The Next Advance in Operation Research :

"Ara hi ha al món màquines que pensen, que aprenen i que creen. A més, la seva capacitat per fer aquestes coses augmentarà ràpidament fins que (en un futur visible) el ventall de problemes que poden gestionar sigui extens amb l'abast al qual s'ha aplicat la ment humana".

Sistemes de prova

Demostrador del teorema de Boyer-Moore (NQTHM)

El disseny de NQTHM va ser influenciat per John McCarthy i Woody Bledsoe. Va començar el 1971 a Edimburg, Escòcia, es tractava d'un demostrador de teoremes totalment automàtic construït amb Pure Lisp. Els principals aspectes de NQTHM van ser:

1. l'ús de Lisp com a lògica de treball.
2. la confiança en un principi de definició per a funcions recursives totals.
3. l'ampli ús de la reescriptura i l'"avaluació simbòlica".
4. una heurística d'inducció basada en el fracàs de l'avaluació simbòlica.

HOL Llum

Escrit a OCaml, HOL Light està dissenyat per tenir una base lògica senzilla i neta i una implementació ordenada. És essencialment un altre assistent de prova per a la lògica clàssica d'ordre superior.

Coq

Desenvolupat a França, Coq és un altre assistent de prova automatitzat, que pot extreure automàticament programes executables de les especificacions, com a codi font Objective CAML o Haskell. Les propietats, els programes i les demostracions es formalitzen en el mateix llenguatge anomenat Càlcul de Construccions Inductives (CIC).

Aplicacions

El raonament automatitzat s'ha utilitzat més habitualment per construir demostradors de teoremes automatitzats. Sovint, però, els demostradors de teoremes requereixen una mica d'orientació humana per ser eficaços i, per tant, de manera més general es qualifica com a ajudants de demostració. En alguns casos, aquests provadors han proposat nous enfocaments per demostrar un teorema. El teòric de la lògica n'és un bon exemple. El programa va presentar una demostració per a un dels teoremes de Principia Mathematica que era més eficient (que requeria menys passos) que la demostració proporcionada per Whitehead i Russell. S'estan aplicant programes de raonament automatitzat per resoldre un nombre creixent de problemes de lògica formal, matemàtiques i informàtica, programació lògica, verificació de programari i maquinari, disseny de circuits i molts altres. El TPTP (Sutcliffe i Suttner 1998) és una biblioteca d'aquests problemes que s'actualitza regularment. També hi ha una competició entre provadors de teoremes automatitzats que se celebra regularment a la conferència CADE (Pelletier, Sutcliffe i Suttner 2002); els problemes per a la competició es seleccionen de la biblioteca TPTP.