Tarskin algoritmi on universaali algoritmi , jonka avulla voit määrittää minkä tahansa suljetun ensimmäisen asteen aritmeettisen kaavan totuuden tai virheellisyyden reaalilukujen muuttujilla . Perustuu Seidenberg-Tarskin lauseeseen .
Tarskin algoritmin avulla voit tarkistaa minkä tahansa väittämän totuuden tai virheellisyyden rajallisesta määrästä reaalilukuja. Tällainen lausunto voidaan kirjoittaa ensimmäisen asteen matemaattisen logiikan standardikielellä. Esittelemällä esimerkiksi karteesiset koordinaatit , mikä tahansa euklidisen geometrian ongelma voidaan pelkistää samanlaiseen muotoon - mikä periaatteessa mahdollistaa minkä tahansa elementaarisen geometrian lauseen automaattisen todistamisen . [1] [2]
On huomattava, että samankaltaiselle kielelle, jossa muuttujat ottavat vain rationaalisia arvoja, Tarskin kaltainen algoritmi ei ole mahdollinen . [yksi]
Algoritmin kehitti vuonna 1948 amerikkalainen logiikka Alfred Tarski . Tällaisen algoritmin olemassaoloa pidettiin pitkään mahdottomana, joten sen luomisesta tuli eräänlainen vallankumous. [3]
Algoritmin alkuperäisen version ajoaikaa ei voitu rajoittaa millään eksponenttitornilla kaavan pituudesta. Myöhemmin algoritmia parannettiin, G. E. Collins ehdotti algoritmia, jonka ajoaika on rajoitettu kaksinkertaiseen eksponenttiin. Käytännössä tämä algoritmi on kuitenkin tehoton. Vuonna 1974 saatiin todiste siitä, että minkä tahansa tämän ongelman algoritmin ajoaika riippuu ainakin eksponentiaalisesti alkuperäisen lauseen pituudesta. [2]