At this moment, Geo III is an unfinished prover for classical logic
with partial functions, based on
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 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.
The latest version is geo2015E.
It can be downloaded from
Note that Geo is released under GNU General Public Licence, Version 3.
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.
- 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.
- Expect input in TPTP-format.
- -include %p
- Use %p as the path, relative to which include files are defined.
TPTP-syntax allows includes.
Develop and implement indexing datastructures,
improve the redundancy strategies, develop decision procedures
with geometric resolution, and make geo generate proof objects.