Tarskiho algoritmus je univerzální algoritmus , který vám umožňuje stanovit pravdivost nebo nepravdivost jakéhokoli uzavřeného aritmetického vzorce prvního řádu s proměnnými pro reálná čísla . Založeno na Seidenbergově-Tarského teorému .
Tarskiho algoritmus vám umožňuje ověřit pravdivost nebo nepravdivost jakéhokoli tvrzení o konečném počtu reálných čísel. Takové prohlášení lze napsat ve standardním jazyce matematické logiky prvního řádu . Zavedením kartézských souřadnic lze například jakýkoli problém euklidovské geometrie zredukovat na podobnou formu – což v zásadě umožňuje automaticky dokázat jakýkoli teorém elementární geometrie. [1] [2]
Je třeba poznamenat, že pro podobný jazyk s proměnnými nabývajícími pouze racionální hodnoty není algoritmus jako Tarski možný . [jeden]
Algoritmus byl vyvinut v roce 1948 americkým logikem Alfredem Tarskim . Existence takového algoritmu byla dlouhou dobu považována za nemožnou, a tak se jeho vytvoření stalo jakousi revolucí. [3]
Doba běhu původní verze algoritmu nemohla být omezena žádnou věží exponentů z délky vzorce. Následně byl algoritmus vylepšen, G. E. Collins navrhl algoritmus, jehož doba běhu je omezena na dvojnásobný exponent. V praxi je však tento algoritmus neúčinný. V roce 1974 byl získán důkaz, že doba běhu jakéhokoli algoritmu pro tento problém závisí přinejmenším exponenciálně na délce původního příkazu. [2]