cocATP 0.2.0
Cristóbal Camarero
University of Cantabria, Spain
Architecture
cocATP is a Coq-inspired [Coq] automated theorem prover made on the free time of the author.
It implements (the non-inductive) part of Coq's logic (calculus of constructions) and syntax.
The proof terms it creates are accepted as proofs by Coq by the addition of
a few definitions (substituting the respective inductive definitions of Coq).
As in Coq, equality and logical connectives other than implication (which is a dependent product of the logic) are defined adding the proper axioms.
The reasoning is tried to be done the more general possible, avoiding to give any special
treatment to both equality and logical connectives.
At difference of most of the other provers, cocATP does not rely on SAT or first-order solver. All reasoning is done in the high-order logic that is the calculus of constructions.
Strategies
The first of the rules is: for a node with conjecture (forall x:T, P x) create a new node with hypothesis (x:T) and conecture (P x).
Other of the major rules consist in: when having a node with conjecture (C) and some hypothesis (H:forall (x1:T1) (x2:T2) ... (xn:Tn), P x1 x2 ... xn), to unificate P with C and prove the Ti necessary. The unification is a subset of the possible high-order unifications. And in this case is a one-sided unification.
There is a lot of other ad-hoc rules and conditions to apply them.
Some of the rules can create existential terms (x:=??:T) alike to Coq's tactic evar.
With these rules resulting proofs are very similar to human-made proofs.
There is a partially implemented second strategy more similar to the ones found in other theorem provers. It consist a saturation algorithm with the high-order modus_ponens. As example, given a hypothesis (P) and another (or the same) hypothesis (forall x:T, Q x), unficate P with T generating a new hypothesis Q. This generalizes the typical saturation rules, as resolution and superposition.
The strategy yet lacks a good conditions for subsumption and simplifcation. Probably it will not be used in competition.
Implementation
cocATP is implemented in Python-2.7 and C. It uses the Ply-3.4 library to
build the parsers for both the Coq and TPTP syntaxes.
Recently, the processing core has been reimplemented in C as a python module, and a python variable controls if using a pure Python or the C version.
Using the C module can be an order of magnitude faster, but it is less tested and introduces the possibility of SEGFAULTS.
Includes a type-verifier of Calculus of Constructions without inductive constructions,
which must be defined with axioms. That is, a buggy partial clone of Coq.
There is support for most of the TPTP syntax, problems are translated to a set of
calculus of constructions terms. cocATP has been specially prepared for THF,
but all the other TPTP formulae without numbers should be accepted.
However cocATP does NOT include a SAT solver, thus it will probably not solve
your trivial cnf problems.
More info at http://www.alumnos.unican.es/ccc66/cocATP.htm
Expected Competition Performance
With the reimplementation of the kernel in C it is expected a great reduction in the execution time, but not a lot of newly solved problems.
References
- Coq
- The Coq development team,
The Coq proof assistant reference manual,
http://coq.inria.fr