Demonstrarea Automată a Teoremelor

SCURT ISTORIC

AL SISTEMELOR DE DEDUCŢIE

Sistemele de deducţie automatã îşi datoreazã apariţia şi existenţa la doi factori principali: progresele realizate în construcţia echipamentelor de calcul pe de-o parte şi sistematizarea capacitatilor umane de a sintetiza concluzii din premise pe de alta. Cum în legatura cu prima componentã care a determinat dezvoltarea sistemelor de deducţie automatã (evoluţia calculatoarelor) existã nenumãrate descrieri, vom discuta în continuare pe scurt cea de-a doua componentã: dezvoltarea sistemelor de deducţie matematicã (automatã). În momentul de faţa, deducţia automatã a devenit o disciplinã fundamentalã nu numai în cadrul inteligenţei artificiale (AI), dar şi în cadrul stiinţei calculatoarelor în general.

Se ştie cã programarea nu numai cã se bazeazã pe logicã (cum s-ã anticipat de Mc Carthy în anii `60) dar poate fi identificatã cu logica. Acest lucru este evident în programarea logicã, unde ecuaţia lui R. Kowalski (1979) îşi gãseşte cea mai potrivitã verificare:

CALCUL (ALGORITM) = DEDUCŢIE + CONTROL.

Obiectivul de a gasi modalitatea generalã de a mecaniza raţionamentele umane şi l-au propus unii matematicieni încã din secolele trecute. De exemplu, în secolul 17, G. W. Leibniz îşi dorea sã dezvolte un limbaj universal (“lingua characteristica”) care sã fie capabil sã exprime orice propoziţie formulate în limbaj natural, chiar dacã aceasta nu are un caracter matematic propriu-zis. Un fragment de calcul în sensul lui Leibniz a fost dezvoltat abia cu 200 de ani mai tarziu, de catre A. de Morgan şi G. Boole. Acesta este ceea ce azi numim calculul propoziţiilor (în 1869 a fost chiar construitã o maşinã empiricã destinatã evaluarii expresiilor booleene).

În 1882 o nouã contribuţie decisive la sistematizarea raţionamentului deductive şi-a adus-o G. Frege, care descrie pentru prima oarã ceea ce azi numim logica prediatelor de ordinul întai. El introduce noţiunile de cuantificatori şi simboluri functionale. Tot G. Frege separã pentru prima oarã noţiunile de sintaxa şi semantica ale unui limbaj formal, separare utilã şi în cazul limbajelor de programare. Ideeile lui G. Frege au fost continuate de catre G. Peano (1889), chiar dacã prin exprimarea unor pasi deductive în limbaj natural, acestea au înregistrat un regres faţã de cele ale primului autor.

Formalizarea raţionamentului logic deductive a constituit un impact puternic în comunitatea matematicã aceasta nefiind receptatã în totalitate ca pozitivã. Doi dintre aparatorii acestei formalizari au fost N. Whitehead şi B. Russel, în carteã lor “Principia Mathematica” (1913) în care se stabileau metodele de eliminare a cuantificatorilor prin introducerea unor simboluri de functii, metode utilizate şi azi în toate sistemele de demonstrare automatã în logica predicatelor. În acelasi an apare cartea lui D. Hilbert şi W. Ackermann, în care se pune prima oarã problema completitudinii calculului predicatelor, problema rezolvatã în 1930 de catre K. Goedel în dizertatia sa. Nedecidabilitatea calculului predicatelor a fost stabilitã independent de A. Turing şi A. Church, în 1936, primul cunoscut ca autor al maşinii abstracte cu acelasi nume, al doilea, ca autor al lambada calculului. Acest rezultat oarecum descurajator, de nedecidabilitate a fost atenuat de rezultatele de semidecidabilitat ale lui J. Herbrand şi T. Skolem: dacã o formulã este validã atunci acest lucru poate fi pus în evidenţã într-un numãr finit de pasi. În caz contrar, fie se poate demonstra nevaliditatea formulei, fie procedurã de demonstrare utilizatã este divergentã sau cicleazã.

Toate aceste studii pot fi considerate ca şi conţinutul “preistoria” demonstrarii automate de teoreme. “Istoria” sa începe cu primele programe scrise în acest scop. De fapt, primele programe de demonstrare automatã au fost scrise odatã cu apariţia primelor calculatoare (anii `50). Astfel, primul autor de programare a fost Martin Davis (1954) şi rezultatul “suprem” obţinut de el (impresionant la aceea data totuşi) a fost cã suma a douã numere pozitive este un numãr pozitiv. Al doilea program a fost prezentat la o conferintã care a avut loc în 1956 la Dartmouth College, timp de douã luni, conferinta consideratã ca locul de nastere al Inteligetei Artificiale. Acest program se numea “Logic Theorist” şi apartinea lui Newell şi Simion de la Carnegie Mellon University. “Istoria orala” a IA relateazã cã editorii de la “Journal of Symbolic Logic” nu au fost impresionati atat de mult de eveniment, ei respingând un articol scris de Newell, Simon şi “Logic Theorist”…Conferinta de la Dartmouth a marcat urmãtorii 20 de ani, când IA a fost dominatã de acei participanti şi de studenţii lor de la MIT, CMU şi Stanford. Numele de IA a fost propus tot acolo de McCarthy.

Un alt eveniment în domeniul demonstratoarelor automate de teoreme (DAT) se considerã cã a început în anul 1958, când tanarul cercetator Wang Hao de la IBM a construit primul DAT prin care a demonstrat 350 de teoreme din “Principia Mathematica”. (De altfel, pentru aceastã realizare el a primit în 1983 premiul acordat de American Mathematical Society). Alte evenimente importante din aceastã perioadã sunt constituite de elaborarea algoritmului Davis-Putnam (1960) şi a noţiunii de unificator, de catre D. Prawitz, (tot în 1960).

Al doilea moment decisiv în evoluţia DAT, care începe o a doua perioadã, îl constituie articolul lui J.A. Robinson. “A masine orientated logic, based on the resoluţion principle”, publicat în Jurnal of ACM, în 1965. Pânã azi, principiul rezolutiei, introdus în acest articol, şi care constituie o generalizare a teoremei lui Herbrand, constituie unul din cele mai utilizate principii care stã la baza constituirii DAT.

Începând cu anul 1965, douã mari directii de cercetare au aparut:

• Rafinarea principiului rezolutiei;

• Introducerea unor metode care sã imite raţionamentul uman.

În ceea ce priveşte prima directie, rezultatele s-au referit la generalizarea principiului (de exemplu prin hiperrezolutie), la reducerea spaţiului soluţiilor posibile (prin utilizarea mulţimii suport) la reprezenarea sub formã de graf a aplicãrii rezolutiei etc.

În ceea ce priveşte o a doua direcţie, aceasta a triumfat în 1980 când limbajele de programare logicã (sau limbajele de programare declarative) au fost definitive acceptate alãturi de limbajele imperative. Se cunoaşte faptul cã în 1981 japonezii au anunţat lansarea proiectului “A cincea generaţie”; în cadrul cãruia performanţa unui calculator urma în decurs de 10 ani sã fie estimatã nu dupã numãrul de operaţii pe secundã ci dupã numãrul de inferenţe (operaţii logice) pe secundã. în [38], “istoria” IA (în cadrul careia DAT ocupã un loc central) este împarţit în urmãtoarele etape:

1943-1956 gestaţia IA;

1952-1966 entuziasm şi mari asteptãri;

1966-1974 o dozã de realism

1974-1980 sisteme bazate pe cunostiinţe,

1980-1988 IA devine industrie.

Evenimentele de dupã 1988 cunosc dese reveniri, mai realiste şi mai eficiente la ideei, mai vechi din “istoria” IA.

Începând din 1980, la aproape toate marile universitaţi au început scrierea unor demonstratoare automate. Vom cita doar demonstratoarele: Markgraf Karl, realizat în Karlsruhe şi Keiserslautern, în 1980, în limbajul LISP, bazat pe metoda rezoluţiei, demonstratorul Reve, scris în 1984 de catre Pierre Lescaune, la Universitatea din Nancy, de asemenea în LISP, şi bazat pe sisteme de rescriere şi demonstratorul RRL scris de Kapur în aceeaşi perioadã în USA. Recent, colectivul de la RISC-Research Institut For Symbolic Computation, Linz, a dezvoltat un demonstrator performant de teoreme, “Theorema”, care foloseşte în prezent Mathematica 3.0.

În momentul de faţã teoria si aplicaţiile în domeniul DAT fac parte integrantã din câteva manifestãri stiinţifice internaţionale cum ar fi: Simpozionul de “Logics în Computer Science” (LICS), “Conference în Automated Deduction” (CADE), conferinţã de “Rewriting Techniques and applicatios” (RTA), conferinţã “Tableaux”, destinatã metodei tabelelor, workshopul anual “Theorema”, care are loc RISC, institutul amintit mai sus, şi toate conferinţele de inteligenţã artificiale. Existã de asemenea reviste dedicate în întregime problemelor de DAT (“Journal of Logic programming”, “Journal of Automated reasoning”, etc.), iar majoritatea revistelor de “Computer science” deţin rubrici permanente în acest domeniu.