Geometric Theorem Proving
Determining Reachability in Petri Nets
Green's Relations for Semigroups
Applications of Gröbner Basis Theory
this page is still in the process of being written
Theorem proving is one of the traditional applications for
Gröbner basis theory. The basic idea is that (by using an affine
co-orninate system) the geometric
conditions shown by a diagram can all be represented as polynomial
equations. So we can represent the hypotheses as h1=0, ...,
hn=0. Any conclusion c=0 can be deduced from the hypotheses if and
only if c is a member of the ideal <h1, ..., hn>. Thus problems such
as proving Pappus' theorem can be expressed as ideal membership
problems - and solved using Gröbner bases.
Petri nets are graphical and mathematical means of modelling the
dynamic behaviour of systems. A Petri net is a bipartite graph with
two types of node - places and transitions. The state of a system is
represented by a marking of the Petri net with tokens at the
places. Transitions represent the events which could potentially
effect the state of the system modelled. The places and transitions
are connected by a flow relation, each transition having input places
and output places. If the input places to a transition all hold tokens
then the transition is enabled, this corresponds to the even being
possible. If the event does occur, then the transition fires, tokens
are removed from the input places and added to the input places. Given
an initial marking of the Petri net it is a key question to find out
what other markings may be reachable through some sequence of events.
Reversiblity corresponds to the ability to reset the device which is
being modelled, this is actually a key feature of some models (e.g.
navigation systems for mobile robots). When the net is reversible, the
reachability problem can be solved using Gröbner bases.
The application of Gröbner bases is achieved by labelling the
places in the net. A marking then is associated to a power product of
place labels raised to the power of the number of tokens held at that
place. If we now represent transitions by difference binomials
i.e. minimum input - minimum output, and let <T> be the ideal they
generate, then we can observe that a
marking M is reachable from the initial marking if and only if the
difference between their representing power products is in the ideal
<T>. This means that by calculating a Gröbner basis for
<T> we can decide which markings are reachable, and in some
circumstances, catalogue all the reachable markings.
Green's relations are a way of expressing the local structure of an
abstract semigroup in terms of groups with certain actions on them.
Eggbox diagrams are used to depict the partitions of a semigroup into
L-classes, R-classes, D-classes and H-classes as defined by Green's
We can sometimes determine the classes by using Gröbner bases
applied directly to the presentation, giving the possibility for
dealing with infinite semigroups having infinitely many H-classes,
L-classes or R-classes.