Algoritmul lui Tarski este un algoritm universal care vă permite să stabiliți adevărul sau falsitatea oricărei formule aritmetice închise de ordinul întâi cu variabile pentru numere reale . Bazat pe teorema Seidenberg-Tarski .
Algoritmul lui Tarski vă permite să verificați adevărul sau falsitatea oricărei afirmații despre un număr finit de numere reale. O astfel de afirmație poate fi scrisă în limbajul standard al logicii matematice de ordinul întâi. Prin introducerea coordonatelor carteziene , de exemplu, orice problemă de geometrie euclidiană poate fi redusă la o formă similară - care, în principiu, permite să se demonstreze automat orice teoremă de geometrie elementară. [1] [2]
Trebuie remarcat faptul că pentru un limbaj similar cu variabile care iau doar valori raționale , un algoritm ca cel al lui Tarski nu este posibil . [unu]
Algoritmul a fost dezvoltat în 1948 de către logicianul american Alfred Tarski . Existența unui astfel de algoritm a fost considerată imposibilă multă vreme, așa că crearea lui a devenit un fel de revoluție. [3]
Timpul de rulare al versiunii originale a algoritmului nu a putut fi limitat de niciun turn de exponenți din lungimea formulei. Ulterior, algoritmul a fost îmbunătățit, G. E. Collins a propus un algoritm al cărui timp de rulare este limitat la un dublu exponent. Cu toate acestea, în practică, acest algoritm este ineficient. În 1974, s-a obținut o dovadă că timpul de rulare al oricărui algoritm pentru această problemă depinde cel puțin exponențial de lungimea instrucțiunii originale. [2]