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

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