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