Geo III
At this moment, Geo III is an unfinished prover for classical logic
with partial functions, based on
Kleene logic.
In the current version, only Chapters 4 and 5 have been implemented,
and the transformation from firstorder logic to geometric logic
is still 2valued.
The goal of Geo III is to implement the complete logic.
I assume that this goal will be reached in the fall of 2015,
because I implemented the hardest part first.
Availability of Geo
Geo will be released shortly after CASC.
Here is a short system description
for CASC 25.
Downloading Geo

The latest version is geo2015E.
It can be downloaded from
CASC.
Note that Geo is released under GNU General Public Licence, Version 3.
Running Geo
In order to run geo, unzip and untar. If you are lucky, you
type './geo < blz202_4.geo' and you see that geo finds a proof.
Otherwise, type 'touch Makefile', type 'make' and hope that
the resulting executable works. You need a reasonably
new version of g++, because Geo uses C++11.
Geo accepts the following parameters:
 inputfile %f.
 Instead of reading from standard input, read from the
indicated file %f.
 nonempty.
 Do not allow empty models. Without this flag, geo cannot prove
forall x. p(x) > exists x. p(x), because the empty model
is a counter model.
 tptp_input.
 Expect input in TPTPformat.
 include %p
 Use %p as the path, relative to which include files are defined.
TPTPsyntax allows includes.
Future Plans
Develop and implement indexing datastructures,
improve the redundancy strategies, develop decision procedures
with geometric resolution, and make geo generate proof objects.