A Geometric Procedure with Prover9
(Web Support)

December 2012

This page provides Web support for A Geometric Procedure with Prover9 [4]. In particular, we present some additional material on the inference rule gL and some proofs that were found with the assistance of the program Prover9 [1].

### Paper Abstract

Here we give an automated proof of the fact that a cubic curve admits at most one group law. This is achieved by proving the tight connection between the chord-tangent law of composition and any potential group law (as a morphism) on the curve. An automated proof of this is accomplished by implementing the rigidity lemma and the Cayley-Bacharach theorem of algebraic geometry as formal inference rules in Prover9, a first-order theorem prover developed by Dr. William McCune.

### gL

For this study, we assume inference rule gL [2][3] in addition to the usual Prover9 inference rules. gL is implemented in Prover9 by including an appropriate set of hyperresolution nuclei as input. An application of gL consists of a hyperresolution step with one of these clauses.

Since gL operates at the term level, there needs to be a separate gL clause for every combination of relevant functions and every possible term position. As a matter of practicality, we limit the nesting level of the gL clauses we include in an input file.

Here is a clause generator for inference rule gL. It takes as arguments a signature and a maximum nesting level. Infix operators are handled by generating prefix versions and then transforming the results with the "Rewriter" program (included in the Prover9 distribution).

Examples:

### Prover9 Proofs

We can require proofs with different properties, depending on various Prover9 settings, for example:

• Whether or not the gL clauses can participate in paramodulation steps, that is, in addition to their use in hyperresolution steps for the application of inference rule gL. See Prover9 flag para_units_only.

• Whether or not the proof steps should consist only of explicit applications of inference rules rather than including rewrite (demodulation) steps. See Prover9 flag back_demod.

• Whether or not the proof should be strictly forward, that is, not including reasoning from the negation of the conclusion of the theorem. See Prover9 flag restrict_denials.

Note that to ensure a strictly forward proof, flag back_demod needs to be cleared -- even if restrict_denials is set -- to prevent back demodulation of the denial of the conclusion.

It typically is more difficult for Prover9 to find a proof with restrictions such as these. In these cases, we can appeal to the method of proof sketches [5] by first finding proofs with fewer restrictions and then using these proofs as hints to help find the desired proofs.

### Results from the Paper

For each proof, we include input, output, proof and xml files created as follows.

prover9 -f file.in > file.out

prooftrans -f file.out > file.pf

prooftrans xml -f file.out > file.xml

Theorem 2, part (1).
(x * y) * x = y =gL=> (x * y) * (z * u) = (x * z) * (y * u).
For the gL clauses, we first used the gL clause generator as follows.
% Signature:  [['f', 2]]
% Clauses to implement gL to nesting level 1
We then used the Rewriter utility to convert f(x,y) terms to the infix form x * y.

Proof. (in, out, pf, xml)

Theorem 3.

{ x * (y * x) = y,
x * y = y * x,
e * e = e,
x + e = x,
e + y = y }

=gL=>

{ (x * y) * e = x + y,
x + (x * e) = e,
x + y = y + x,
x + (y + z) = (x + y) + z }
The following proof is the basis for the proof presented in the paper. It relies on a single selected gL clause and is restricted to be strictly forward and demodulation free. The input file includes hints from previously found proofs (that is, from runs with a larger set of gL clauses and/or fewer restrictions).

Proof. (in, out, pf, xml)

Here is the original proof of Theorem 3. It was run with a complete set of gL clauses for x * y and x + y up to nesting level 1 and without any input hints. Prover9 was run without the paramodulation unit, strictly-forward or demodulaton-free restrictions.

Proof. (in, out, pf, xml)

Theorem 4.
{ f(e, e, e) = e,
f(x, y, z) = f(x, z, y),
f(x, y, f(x, y, z) ) = z,
x + e = x,
e + x = x }

=gL=>

{ x + y = f(e, e, f(e, x, y)).
x + f(e, x, e) = e }
As discussed in the paper, we formulated the problem to have Prover9 "discover" the form of the inverse by including the clause,
A + y != e.
rather than including the second goal,
x + f(e, x, e) = e.
explicitly. In addition, a clause that subsumes the first goal,
x + y = f(e, e, f(e, x, y)).
appears in the proof of the second goal, so an independent proof is not needed.

The following proof is the basis for the proof presented in the paper. It is restricted to be strictly forward and demodulation free and includes an answer literal to identify the inverse term. The input file includes hints from the original proof (below) which was run with an additional assumption and with fewer restrictions.

In this case, we include only the input and output files simply because the rewriter utility doesn't support the answer literal. The proof is easily seen by inspection of the output file.

Proof. (in, out)

Here is the original proof used to find the proof of Theorem 4. It was run with a complete set of gL clauses for f(x,y,z) and x + y up to nesting level 1 and without any input hints. Prover9 was run without the strictly-forward or demodulaton-free restrictions. An additional assumption,

f(x, y, z) = f(y, z, x).
was included because this is the theorem we originally were trying to prove. The stronger version (without the assumption) that appears in the paper was identified later.

Proof. (in, out, pf, xml)

### References

1. W. McCune. Prover9. http://www.cs.unm.edu/~mccune/prover9.
2. W. McCune and R. Padmanabhan. Automated deduction in equational logic and cubic curves. Lecture Notes in Artificial Intelligence 1095, Springer-Verlag, Berlin, 1996.
3. R. Padmanabhan and W. McCune. Automated reasoning about cubic curves. Computers and Mathematics with Applications 29(2):17-26, 1995.
4. R. Padmanabhan and R. Veroff. A Geometric Procedure with Prover9. Submitted for publication.
5. R. Veroff. Solving Open Questions and Other Challenge Problems Using Proof Sketches. Journal of Automated Reasoning, 27(2):157-174, 2001. (postscript)