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 a paper at IJCAR 2006 by
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.
The latest version is geo2007F.
It can be downloaded by clicking
Note that Geo is released under GNU General Public Licence, Version 3.
Previous geo2006j is available
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.
- 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.
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.