boi@uicsl.UUCP (11/01/84)
( for the line eater)
I have recently discovered an interesting old (1951) paper by A. Tarski
describing a general decision method for elementary algebra. His algorithm
has the interesting property that it is based on a method for converting
quantified formulas into equivalent ones without quantifiers.
For example, one can convert the expression
(exists x)[a0 + a1*x + a2*x**2 + a3*x**3 = 0]
into the equivalent expression:
{ (a0=0) v [~(a1=0) ^ (a2=0)] v [~(a2=0)^~(4*a0*a2 > a1**2)] v ~(a3=0)}
The whole thing is based on some general version of what is called
Sturm's theorem, which basically allows you to tell how many solutions
some system of equations has. Unfortunately, the original method gives
rather huge equivalent expressions.
Does anybody out there know of any more recent work on these things?
I presume someone must have expanded the original results by now.
Please let me know of any pointers you may have.
Boi Faltings
Coordinated Science Lab.
1101 W. Springfield Ave.
Urbana, Il. 61801