FOM: Axiomatizing plane geometry - a notion of convexity?

[Duraid Madina]

Hi all,

	I've got a simple problem - I want to 'encode' a set of points in the 
plane in a format suitable for input to a SAT (satisfiability) solver - in 
my case, I've got AND, OR, NOT, -> (implies), <-> (bi-implies) () 
(bracketing!) and boolean variables.

	I've got the guarantee that moving along the set of points, one _always_ 
turns left or right - another way of saying this is that no three of the 
points are collinear.

	Now I know that there are only so many configurations of n points in the 
plane (proportional to 2^n, I suspect?) - I'm guessing (hoping) the number 
of boolean variables I'll need is proportional to n by some constant 
factor. At any rate, what I'm *really* wondering is:

	Can anyone think of a way of forming a proposition using the operations 
I've listed above such that given some _assignment_ of {0,1} to the 
variables (thus describing some configuration of n points in the plane), 
the proposition will be true if and only if the points can form a convex 
m-gon? Obviously if m=3 the propositions formed will always be true, and if 
m>n they'll never be true.

	Many thanks in advance,

	Duraid