Geo is a prover for full-first order logic. It is writen in C++. It is based on a new calculus, which is called geometric resolution, and which is described in this paper, which was published at IJCAR 2006. The calculus is called geometric resolution, because it uses an internal format that is closely related to geometric logic. It should be equally good at finding proofs as at finding finite models. Here is a short system description that was written for CASC 21.

Downloading Geo

The last 2-valued version is geo2007F. It can be downloaded by clicking 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 type ./geo < examples/blz202_4.geo and you see that geo finds a proof. Otherwise, type 'touch Makefile', type 'make' and hope that the resulting executable works. 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.