Geo III (2015E)
Hans de Nivelle
University of Wrocław, Poland
Geo III is a theorem prover for
Partial Classical Logic, based
Currently, only Chapters 4 and 5
Since Kleene logic generalizes 2-valued logic, it is
still possible to take part in CASC.
Apart from being 3-valued, the main differences with earlier
versions of Geo are (1) more sophisticated learning schemes,
(2) improved proof logging, and (3) replacement of
recursion by explicit use of a stack.
The Geo family of provers uses exhaustive backtracking, combined with
learning after failure. Earlier versions learned only conflict formulas.
Geo III learns disjunctions of arbitrary width.
Experiments show that this often results in shorter proofs.
If Geo will be ever embedded in proof assistants, these assistants
will require proofs. In order to be able to provide
these at the required level of detail, Geo III contains a
hierarchy of proof rules that is independent of the
rest of the system, and that can be modified independently.
In order to be flexible in the main loop, recursion was replaced
by an explicit stack. Using an explicit stack, it is easier to
remove unused assumptions, or to rearrange the order of assumptions.
Also, restarts are easier to implement with a stack.
Geo uses breadth-first, exhaustive model search,
combined with learning. In case of branching,
the branches are explored in random order.
Specially for CASC, a restart strategy was added, which ensures
that proof search is always restarted after 4 minutes.
This was done because Geo III has no indexing. After some
time, proof search becomes so inefficient that it makes no sense
to continue, so that it is better to restart.
Geo III is written in C++ 11. No features outside of the standard
were used. It has been tested with
g++ (version 4.8.4) and with
Version 2015E contains almost no technical optimizations, because
the calculus (the geometric format, the learning schemes,
and the restart strategies) are not yet mature.
Expected Competition Performance
We view CASC as a free test. Hence we will
not make any predictions.