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.

Running Geo

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: