Geo
Geo
Geo is a prover for fullfirst order logic.
It is writen in C++.
It is based on a new calculus, which is called geometric resolution,
and which is described in a paper at IJCAR 2006 by
Jia Meng
and me.
The calculus is called geometric resolution, because it uses
an internal format that is closely related to geometric logic.
It should be equally good in finding proofs as in finding finite models.
Availability of Geo
Geo will be released shortly after CASC.
Here is a short system description
for CASC 25.
Downloading Geo

The latest version is geo2007F.
It can be downloaded by clicking
here .
Note that Geo is released under GNU General Public Licence, Version 3.

Previous geo2006j is available
here .
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.
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 TPTPformat.
Some Future Plans
Some things that should be done are: Develope indexing datastructures,
improve the redundancy strategies, develope decision procedures
with geometric resolution, and make geo generate proof objects.