Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: Notesfiles $Revision: 1.6.2.17 $; site uicsl.UUCP
Path: utzoo!watmath!clyde!burl!ulysses!mhuxj!ihnp4!inuxc!pur-ee!uiucdcs!uicsl!boi
From: boi@uicsl.UUCP
Newsgroups: net.ai
Subject: Tarski's decision method
Message-ID: <12300005@uicsl.UUCP>
Date: Wed, 31-Oct-84 22:44:00 EST
Article-I.D.: uicsl.12300005
Posted: Wed Oct 31 22:44:00 1984
Date-Received: Fri, 2-Nov-84 06:09:27 EST
Lines: 30
Nf-ID: #N:uicsl:12300005:000:1230
Nf-From: uicsl!boi    Oct 31 21:44:00 1984

( 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