Tarskis algoritm är en universell algoritm som låter dig fastställa sanningen eller falskheten i alla stängda första ordningens aritmetiska formel med variabler för reella tal . Baserat på Seidenberg-Tarski-satsen .
Tarskis algoritm låter dig kontrollera sanningen eller falskheten i ett påstående om ett ändligt antal reella tal. Ett sådant påstående kan skrivas på standardspråket för matematisk logik av första ordningen . Genom att introducera kartesiska koordinater , till exempel, kan alla problem med euklidisk geometri reduceras till en liknande form - vilket i princip gör att man automatiskt kan bevisa vilken sats som helst av elementär geometri. [1] [2]
Det bör noteras att för ett liknande språk med variabler som endast tar rationella värden, är en algoritm som Tarskis inte möjlig . [ett]
Algoritmen utvecklades 1948 av den amerikanske logikern Alfred Tarski . Förekomsten av en sådan algoritm ansågs omöjlig under lång tid, så dess skapelse blev en slags revolution. [3]
Körtiden för den ursprungliga versionen av algoritmen kunde inte begränsas av något torn av exponenter från formelns längd. Därefter förbättrades algoritmen, G. E. Collins föreslog en algoritm vars körtid är begränsad till en dubbel exponent. Men i praktiken är denna algoritm ineffektiv. År 1974 erhölls ett bevis för att körtiden för någon algoritm för detta problem åtminstone exponentiellt beror på längden på det ursprungliga uttalandet. [2]