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 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.

Downloading Geo

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 TPTP-format.
-include %p
Use %p as the path, relative to which include files are defined. TPTP-syntax 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.