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 first-order logic to geometric logic is still 2-valued. The goal of Geo III is to eventually implement the complete logic.
The latest version is geo2016C. It can be downloaded from here. Geo is released under GNU General Public Licence, Version 3.
In order to run geo, unzip and untar. If you are lucky, you
can type ./geo < testexamples/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 TPTP-format.
-include %p Use %p as the path, relative to which include files are defined. TPTP-syntax allows includes.