Grigori Mints

Grigori Mints, ka Grisha Mints (vene keeles Григорий Эфраимович Минц; 7. juuni 1939 Leningrad – 29. mai 2014 Palo Alto, California) oli Nõukogude Liidu ja Ameerika Ühendriikide loogik, arvutiteadlane ja matemaatik.
Grigori Mints oli rahvusvaheliselt tuntud loogik ja arvutiteadlane, kelle tööd tõestusteoorias on leidnud otsest rakendust arvutiteaduses. Ta on andnud olulise panuse Eesti arvutiteadusse. Tema õpilased on Tallinna Tehnikaülikooli professor Tanel Tammet ja akadeemik Tarmo Uustalu.
Ta oli Stanfordi Ülikooli professor ja Eesti Teaduste Akadeemia välisliige.
Haridustee.
Grigori Mints lõpetas 1961. aastal Leningradi Riikliku Ülikooli matemaatika erialal ning kaitses 1965. aastal sama ülikooli juures füüsika-matemaatikakandidaadi ja 1990. aastal füüsika-matemaatikadoktori kraadi (doktoriväitekiri "Преобразования доказательств и синтез программ").
Karjäär.
Enne Eestit.
Aastatel 1961–1979 töötas Grigori Mints vanemlaborandi ja nooremteadurina NSV Liidu TA V. A. Steklovi nimelise Matemaatika Instituudi Leningradi osakonnas. Ühtlasi töötas ta aastatel 1962–1979 Leningradi Riiklikus Ülikoolis, kus õpetas põhiosa loogikakursustest.
Tema teadushuvid haarasid matemaatilist loogikat (põhirõhuga tõestusteoorial), asendusmeetodit, dünaamilist topoloogilist loogikat, konstruktiivset matemaatikat. Grigori Mints kuulus Leningradi tõestuste teooria koolkonda. Koos kolleegidega lõi ta klassikalise loogika tarbeks tõestuse otsingu strateegiad ja nende rakendamise programmid, sealhulgas esimese loomuliku keele kasutajaliidesel põhineva loomuliku tuletamise programmi (1964).
Eestis.
1970. aastate lõpul esines Grigori Mints Tartu Riikliku Ülikooli programmeerimise kateedri ja Teaduste Akadeemia Küberneetika Instituudi ühises suvekoolis Pärnu lähedal Elbis. Loengute teemaks oli algoritmide ajaline keerukus. 1981. aastal asus ta juba elama ja tööle Eestisse, kus ta oli aastatel 1981–1991 TA Küberneetika Instituudi vanemteadur.
Grigori Mints ja Tanel Tammet leidsid ja realiseerisid koostöös uued tõestusvõtted teoreemide automaatseks tõestamiseks klassikalise loogika raames. Tõestusteooriauurimused on leidnud rakendust arvutiteaduses, sealhulgas ka Eestis loodud programmeerimissüsteemides PRIZ ja NUT.
Mints on teinud koostööd ka Enn Tõugu töögrupiga, koos töötasid nad välja arvutusmudelite ja programmide sünteesi formaalloogilised esitused, mis pakkusid suurt huvi loogikutele.
Mintsi Küberneetika Instituudi perioodi tegemiste haare oli suur: kolleegidele loogikatõdede õpetamine, uurimisprojektides osalemine, programmide sünteesi loogilisi aluseid selgitava trükise avaldamine, loengute pidamine, teadusürituste korraldamine ja rahvusvaheliste teaduskontaktide edendamine. Tema õpilased on Tanel Tammet, hilisem Tallinna Tehnikaülikooli professor, ja Tarmo Uustalu, hilisem Eesti Teaduste Akadeemia akadeemik.
1991. aastal töötas Mints lühemat aega osakoormusega professorina Tartu Riikliku Ülikooli programmeerimise kateedris, kus ta õpetas tõestuste teooria kursust.
Pärast Eestit.
1991. aastal valiti Grigori Mints Stanfordi Ülikooli professoriks filosoofia alal. Hiljem lisandusid samas ülikoolis veel arvutiteaduse (1992) ja matemaatika professori ametikohustused (1997).
Grigori Mints on töötanud külalisprofessorina tippülikoolides, nagu Kuninglik tehnikaülikool Stockholmis, California Ülikool Berkeleys, Müncheni ülikool kui ka nõustajana Californias Palo Altos asuvas Kestreli Instituudis. Ta oli paljude doktoriväitekirjade juhendaja. Tema sulest on ilmunud üle 3000 retsensiooni tuntud referaatajakirjadele, sealhulgas ajakirjadele Mathematical Reviews, Zentralblatt für Mathematik, Computer Abstracts ja ("Реферативный Журнал : Математика").
2009. aastal külastas Mints Venemaa TA Steklovi-nimelise matemaatika instituudi Peterburi osakonna matemaatilise loogika laboratooriumi. USA teadlase viiepäevast teaduskäiku rahastas Dmitri Zimini Fond Dünastia programmi "Välisteadlaste lühiajalised visiidid Venemaale" raames.