Geo III (2015E)

Hans de Nivelle
University of Wrocław, Poland

Architecture

Geo III is a theorem prover for Partial Classical Logic, based on reduction Kleene Logic . Currently, only Chapters 4 and 5 are implemented. 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.
  1. 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.
  2. 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.
  3. 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.

Strategies

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.

Implementation

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