Tarski: A System for computing with Tarski Formulas and Semi-Algebraic Sets

Tarski is a system that provides an interface to a number of functions for computing with Tarski formulas and semi-algebraic sets. Right now, the system and its functionality are in an early stage of development, but the goal is to provide a an environment for creating and testing new algorithms and, ultimately, to produce a system that is flexibly able to choose efficient solution strategies for a wide range of Tarski formula problems.

In its current stage, some of the primary pieces of functionality it offers are:;

Installation Download tarski1.28.tar.gz and unpack. Follow the directions in the root directory's README to compile.

Example 
~/$ tarski
> (def F1 [ y > -x (x - 1) /\ (x - 1/3)^2 + y^2 < (1/2)^2 ])   ; define F1 as a formula
:void
> (def R1 (SAT-NuCADConjunction F1))                           ; determine (open) satisfiability of F1
:void
> (head R1)
( ( x:sym y:sym ) ( 0:num 1/8:num ) )
> (def F2 [ y > -x (x - 1) /\ (x - 1/3)^2 + y^2 < (1/8)^2 ])   ; define F2 as a formula
:void
> (def R2 (SAT-NuCADConjunction F2))                           ; determine (open) satisfiability of F2
:void
> (head R2)
false:boo
> (def F [ y > -x (x - 1) /\ (x - c)^2 + y^2 < r^2 /\ r > 0 ]) ; F generalizes with parameters
:void
> (def D (make-NuCADConjunction '(c r x y) '(0 0 0 0) F))      ; construct an open NuCAD for F
:void
> (msg D 'project 2)                                           ; project onto (c,r)-space
:void
> (msg D 'plot-leaves "-1 1 -1 1 500 500" "C" "/tmp/foo.svg")  ; produce a plot
:void
> (msg D 'negate)                                              ; swap true/false labels on the cells of D
:void
> (msg D 'def-form)                                            ; get a defining formula for D
"[ [ r < _root_1 r ] \/ [ r > _root_1 r /\ r < _root_2 16 r^6 - 48 c^2 r^4 + 48 c r^4 - 13 r^4 
+ 48 c^4 r^2 - 96 c^3 r^2 + 92 c^2 r^2 - 44 c r^2 + 8 r^2 - 16 c^6 + 48 c^5 - 52 c^4 + 24 c^3 - 4 c^2  
/\ c > _root_1 c /\ c < _root_1 2 c - 1 ] \/ [ r > _root_1 r /\ r < _root_2 16 r^6 
- 48 c^2 r^4 + 48 c r^4 - 13 r^4 + 48 c^4 r^2 - 96 c^3 r^2 + 92 c^2 r^2 - 44 c r^2 + 8 r^2 - 16 c^6 
+ 48 c^5 - 52 c^4 + 24 c^3 - 4 c^2  /\ c > _root_1 2 c - 1 /\ c < _root_1 c - 1 ] ]":str
> (quit)
~/$