Tarski Geometry - MathMorphs

[luciano graphic] By Luciano (luciano@core-sdi.com)

Keywords: Squeak, MathMorphs, Tarski Geometry, Tarski Sentences, Tarski Sets, Real Algebraic Geometry, Real Geometry, Semialgebraic Sets, Sturm Theory, Real Quantifier Elimination, Cylindrical Algebraic Decomposition, CAD.

This is my MathMorph project on Tarski geometry. Roughly, I implemented the Cylindrical Algebraic Decomposition (CAD) algorithm, which generalizes the Sturm algorithm to R^n. I use the CAD of a polynomial set to decide the truth of Tarski sentences. The current implementation involves (among others) the following classes:

Tuple
Matrix
Polynomial
PolynomialSet
PolynomialEquation
PolynomialInequality
MonomialOrdering
AlgebraicNumber
CylindricalAlgebraicDecomposition
RealInterval
SemialgebraicCell
SemialgebraicSet
BooleanConnective
ConjuntionConnective
DisjunctionConnective
ImplicationConnective
ConnectivityGraph
Quantifier
ExistentialQuantifier
UniversalQuantifier
QuantifiedSentence

If you are looking for implementation details, just download the change set and use a class browser. There are a few examples in the class comments. You will probably find bugs. If so, please tell me.

The following are two references on the subject you might find useful:

Bhubaneswar Mishra, "Algorithmic Algebra", Springer-Verlag, 1993.
J.T. Schwartz and M. Sharir, "Algorithmic Motion Planning in Robotics", chapter 8 in "Handbook of Theoretical Computer Science, volume A: Algorithms and Complexity", 391--430 pp., edited by J. van Leeuwen, MIT Press, 1994.

Click here to download the change set.

Enjoy and take it easy.