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