Dovada automată a teoremelor

Dovedirea automatizată a teoremelor (în engleză Automated theorem proving sau ATP) sau deducerea automată este cel mai dezvoltat subdomeniu al raționamentului automat . Operația constă în demonstrarea teoremelor matematice de către un program de calculator .

Definiție

Tehnicile de calcul automat ale teoremei constau în aplicarea metodelor de calcul la dovada teoremelor. În general, procedura este următoarea:

Teorema de demonstrat este convertită în termeni algebrici: atât ipoteza, cât și teza sunt exprimate ca condiții de tip $P_{i}(x_{1},\ldots ,x_{n})=0,i=1,\ldots ,k$ ${\ displaystyle P_ {i} (x_ {1}, \ ldots, x_ {n}) = 0, i = 1, \ ldots, k}$ ${\ displaystyle P_ {i} (x_ {1}, \ ldots, x_ {n}) = 0, i = 1, \ ldots, k}$ Și $Q(x_{1},\ldots ,x_{n})=0$ ${\ displaystyle Q (x_ {1}, \ ldots, x_ {n}) = 0}$ ${\ displaystyle Q (x_ {1}, \ ldots, x_ {n}) = 0}$ respectiv.
Prin urmare, veridicitatea teoremei este echivalentă cu aceea $Q\,$ ${\ displaystyle Q \,}$ ${\ displaystyle Q \,}$ este în idealul generat de $P_{1},\ldots ,P_{k}$ ${\ displaystyle P_ {1}, \ ldots, P_ {k}}$ ${\ displaystyle P_ {1}, \ ldots, P_ {k}}$ (echivalent cu anularea $P_{1},\ldots ,P_{k}$ ${\ displaystyle P_ {1}, \ ldots, P_ {k}}$ ${\ displaystyle P_ {1}, \ ldots, P_ {k}}$ la un moment dat are ca rezultat anularea $Q\,$ ${\ displaystyle Q \,}$ ${\ displaystyle Q \,}$ în același punct) ..

Cu toate acestea, aceea a apartenenței unui polinom la un ideal este o problemă clasică a algebrei de calcul ; o tehnică comună pentru rezolvarea acestei probleme este calculul unei baze Gröbner adecvate. Această metodă are dezavantajul unei complexități de calcul ridicate.

Evoluția istorică

În timp ce rădăcinile logicii formalizate se întorc la Aristotel, perioada cuprinsă între sfârșitul secolului al XIX-lea și începutul secolului al XX-lea a văzut dezvoltarea logicii moderne și a matematicii formalizate. Cartea lui Gottlob Frege Begriffsschrift (1879) a introdus atât un calcul propozițional complet , cât și o logică de predicat esențial modernă ^[1] . Die Grundlagen der Arithmetik (Fundamentele aritmeticii) , publicat în 1884 ^[2] , a exprimat părți ale matematicii în logică formală. Această abordare a fost continuată de Russell și Whitehead în influenta lor Principia Mathematica , publicată pentru prima dată între 1910 și 1913 ^[3] și cu o a doua ediție revizuită în 1927 ^[4] . Russell și Whitehead au crezut că pot obține toate adevărurile matematice folosind axiome și reguli de inferență ale logicii formale, începând în principiu procesul de automatizare. În 1920, Thoralf Skolem a simplificat un rezultat anterior al lui Leopold Löwenheim , ducând la teorema Löwenheim-Skolem și, în 1930, la noțiunea de Univers Herbrand și Interpretarea Herbrand, care a permis reducerea satisfacției (sau nu) a primului ordin de formule ( și, prin urmare, validitatea unei teoreme) la mai multe (potențial infinite) probleme de satisfacție în termeni propoziționali ^[5] . În 1929, Mojżesz Presburger a arătat că teoria numerelor naturale cu adunare și egalitate (numită acum aritmetică Presburger în onoarea sa) este decisă și a furnizat un algoritm capabil să determine dacă o propoziție dată în limbă era adevărată sau falsă ^[6] ^[7] . Cu toate acestea, la scurt timp după acest rezultat pozitiv, Kurt Gödel a publicat „ Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I ” („Despre propunerile formal nedecidabile ale principiilor matematicii și sistemelor conexe”) (1931), dovedind că în orice axiomatică sistem suficient de puternic există afirmații adevărate care nu pot fi dovedite în cadrul sistemului. Acest argument a fost dezvoltat în continuare în anii 1930 de Alonzo Church și Alan Turing , care, pe de o parte, au dat două definiții independente, dar echivalente, ale calculabilității și, pe de altă parte, au oferit exemple concrete de probleme indecidabile. La scurt timp după al doilea război mondial, primele computere au devenit disponibile. În 1954, Martin Davis a programat algoritmul Presburger pentru un computer tub cu vid JOHNNIAC la Princeton Institute for Advanced Studies . Potrivit lui Davis, „marele său triumf a fost să demonstreze că suma a două numere pare este pare” ^[7] ^[8] . Mai ambițios a fost Logic Theorist , un program de deducție logică propozițională din Principia Mathematica , dezvoltat de Allen Newell, Herbert A. Simon și JC Shaw. Mai mult, teoreticianul logicii, care rulează pe JOHNNIAC, a construit dovezi dintr-o serie mică de axiome propoziționale și din trei reguli de deducere: modus ponens , înlocuirea unei variabile propoziționale și înlocuirea formulelor cu definiția lor. Sistemul a folosit ghidul euristic și a putut dovedi 38 din primele 52 de teoreme ale Principiei ^[7] . Abordarea „euristică” a sistemului teoretic al logicii a încercat să imite matematicienii umani și nu a putut garanta că se poate găsi o dovadă pentru orice teoremă valabilă, chiar și în principiu. În schimb, alți algoritmi mai sistematici au obținut, cel puțin teoretic, completitudinea logicii de ordinul întâi . Abordările inițiale s-au bazat pe rezultatele lui Herbrand și Skolem pentru a converti o formulă de ordinul întâi în grupuri succesiv mai mari de formule propoziționale, instanțierea variabilelor cu termeni din universul Herbrand. Insuficiența formulelor propoziționale ar putea fi testată folosind o serie de metode. Programul lui Gilmore a folosit conversia în formă normală disjunctivă , o formă în care satisfacția unei formule este suficientă ^[7] ^[9] .

Notă

^ Gottlob Frege, Begriffsschrift , Verlag Louis Neuert, 1879.
^ Gottlob Frege, Die Grundlagen der Arithmetik ( PDF ), Breslau, Wilhelm Kobner, 1884 (arhivat din original la 10 iunie 2007) .
^ Bertrand Russell și Alfred North Whitehead, Principia Mathematica , 1st, Cambridge University Press, 1910–1913.
^ Bertrand Russell și Alfred North Whitehead, Principia Mathematica , 2, Cambridge University Press, 1927.
^ Jaques Herbrand, Recherches sur la théorie de la démonstration , 1930.
^ Mojżesz Presburger, Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt , în Comptes Rendus du I congrès de Mathématiciens des Pays Slaves , Warszawa, 1929, pp. 92-101.
^ ^a ^b ^c ^d Martin Davis , The Early History of Automated Deduction ( ps ), în Alan Robinson și Andrei Voronkov (eds), Handbook of Automated Reasoning , vol. 1, Elsevier , 2001. )
^ Wolfgang Bibel, Early History and Perspectives of Automated Deduction ( PDF ), în KI 2007 , LNAI, n. 4667, Springer, 2007, pp. 2-18. Accesat la 2 septembrie 2012 .
^ Paul Gilmore, A procedure procedure for quantification theory: its justification and realization , în IBM Journal of Research and Development , vol. 4, 1960, pp. 28–35, DOI : 10.1147 / rd.41.0028 .

Elemente conexe

Rationament automat

Controlul autorității	LCCN ( EN ) sh85010111

Portal IT

Portalul de matematică

[1] Gottlob Frege, Begriffsschrift , Verlag Louis Neuert, 1879.

[2] Gottlob Frege, Die Grundlagen der Arithmetik ( PDF ), Breslau, Wilhelm Kobner, 1884 (arhivat din original la 10 iunie 2007) .

[3] Bertrand Russell și Alfred North Whitehead, Principia Mathematica , 1st, Cambridge University Press, 1910–1913.

[4] Bertrand Russell și Alfred North Whitehead, Principia Mathematica , 2, Cambridge University Press, 1927.

[5] Jaques Herbrand, Recherches sur la théorie de la démonstration , 1930.

[6] Mojżesz Presburger, Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt , în Comptes Rendus du I congrès de Mathématiciens des Pays Slaves , Warszawa, 1929, pp. 92-101.

[Davis2001-7] Martin Davis , The Early History of Automated Deduction ( ps ), în Alan Robinson și Andrei Voronkov (eds), Handbook of Automated Reasoning , vol. 1, Elsevier , 2001. )

[Bibel2007-8] Wolfgang Bibel, Early History and Perspectives of Automated Deduction ( PDF ), în KI 2007 , LNAI, n. 4667, Springer, 2007, pp. 2-18. Accesat la 2 septembrie 2012 .

[9] Paul Gilmore, A procedure procedure for quantification theory: its justification and realization , în IBM Journal of Research and Development , vol. 4, 1960, pp. 28–35, DOI : 10.1147 / rd.41.0028 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]