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. 61801yun@smu (11/09/84)
Plenty of work has been done since then. E.g. George Collins of U. Wisconsin
spent much of career trying to make Tarski's decision procedure efficient, or
just computable for any "non-toy" problems. Recently, some complexity results
were discovered (bad news, doubly exponential). References can be found in
SYMSAC Proc. '71 or 76.
D. Y. Y. Yun, CS&E/SMU