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].
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:
We can require proofs with different properties, depending on various Prover9 settings, for example:
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.
For each proof, we include input, output, proof and xml files created as follows.
prover9 -f file.in > file.outprooftrans -f file.out > file.pf
prooftrans xml -f file.out > file.xml
(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 1We then used the Rewriter utility to convert f(x,y) terms to the infix form x * y.
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).
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.
{ 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.
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.