Geo

Hans de Nivelle
nivelle[at]mpi-sb[dot]mpg[dot]de
Jia Meng
jia[dot]meng[at]mail[dot]rsise[dot]anu[dot]edu[dot]au

Architecture

Geo is based on geometric resolution. A geometric formula is a formula with form:
Forall x1, ..., xn A1 /\ ... /\ Ap /\ v1 != w1 /\ ... /\ vq != wq -> Z(x1,...,xn).

The Ai must be non-equality atoms. The arguments of the atoms Ai must be among the variables x1, ..., xn. There are no function symbols, and no constants in the atoms Ai. The inequalities vj != wj must have their arguments among x1, ..., xn.
Z(x1,...,xn) must have one of the following three forms:

  1. The false constant FALSE.
  2. A disjunction B1 \/ ... \/ Br. The atoms Bk must be non-equality atoms. The arguments of the atoms Bk are among the variables x1, ..., xn. There are no function symbols, and no constants in the atoms Bk.
  3. An existential quantification EXISTS y B. y is a variable distinct from x1,...,xn. B is an atom which has all arguments among x1,...,xn,y.
As input, Geo accepts geometric formulas and first-order formulas. First-order formulas are transformed into geometric formulas. During this translation, function symbols have to be removed, and replaced by relations.

During search, Geo searches for a model of the geometric formulas by backtracking. At each choice point, after all subbranches have been refuted, it derives a new rule of Type 1, which refutes the current model attempt without backtracking. In this way, Geo learns during backtracking. In case Geo finds a finite model, it simply prints the model. In case no model exists, it will eventually learn the rule -> FALSE, so that it is able to output a refutation proof. The final aim of geometric resolution, and of Geo, is to obtain a prover that is both good at finding proofs, and at finding finite models.

Implementation

Geo is written in C++. We try to keep the code readable and reasonably efficient at the same time.

Strategies

Currently, Geo has only one strategy: It searches for a model by exhaustive search, and learns a new rule at each choice point, after it has refuted all subbranches. There are still many uncertainties in the way geometric resolution has to be implemented, and Geo is only a first attempt.

Expected Competition Performance

Geo was completed too short before the competition. We have not done big testing, so we cannot predict the performance.