Geo
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:
-
The false constant FALSE.
-
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.
-
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.