logic - Prover9 hints not being used

Question

I'm running some Lattice proofs through Prover9/Mace4. I'm using a non-standard axiomatization of the lattice join operation, from which it is not immediately obvious that the join is commutative, associative and idempotent. (I can get Prover9 to prove that it is -- eventually.)

I know that Prover9 looks for those properties to help it search faster. I've tried putting those properties in the Additional Input section (I'm running the GUI version 0.5), with

formulas(hints).
x v y = y v x.
% etc
end_of_list.

Q1: Is this the way to get it to look at hints?

Q2: Is there a good place to look for help on speeding up proofs/tips and tricks? (If I can get this to work, there are further operators I'd like to give hints for.)

For ref, my axioms are (bi-lattice with only one primitive operation):

x ^ y = y ^ x.                % lattice meet
x ^ x = x.
(x ^ y) ^ z = x ^ (y ^ z).
x ^ (x v y) = x.              % standard absorption for join
x ^ z = x & y ^ z = y <-> z ^ (x v y) = (x v y).
                              % non-standard absorption

(EDIT after DougS's answer posted.)

Wow! Thank you. Orders-of-magnitude speed-up.

Some follow-on q's if I might ...

Q3: The generated hints seem to include all of the initial axioms plus the goal -- is that what I should expect? (Presumably hence your comment about not needing all of the hints. I've certainly experienced that removing axioms makes a proof go faster.)

Q4: What if I add hints that (as it turns out) aren't justified by the axioms? Are they ignored?

Q5: What if I add hints that contradict the axioms? (From a few trials, this doesn't make Prover9 mis-infer.)

Q6: For a proof (attempt) that times out, is there any way to retrieve the formulas inferred so far and recycle them for hints to speed up the next attempt? (I have a feeling in my waters that this would drag in some sort of fallacy, despite what I've seen re Q3 and Q4.)

Answer 1

Q1: Yes, that should work for hints. But, to better test it, take the proof you have, and then use the "reformat" option and check the "hints" part. Then copy and paste all of those hints into your "formulas(hints)." list. (well you don't necessarily need them all... and using only some of them might lead to a shorter proof if it exists, but I digress). Then run the proof again, and if it runs like my proofs in propositional calculi with hints do, you'll get the proof "in an instant".

Just in case... you'll need to click on the "additional input" tab, and put your hint list there.

Q2: For strategies, the Prover9 manual has useful information on weighting, hints, and semantic guidance (I haven't tried semantic guidance). You might also want to see Bob Veroff's page (some of his work got done in OTTER, but the programs are similar). There also exists useful information Larry Wos's notebooks, as well as Dr. Wos's published work, though all of Wos's recent work has gotten done using OTTER (again, the programs are similar).

Answer 2

Q3: Yes, you should expect the axiom(s) and the goal(s) included as hints. Both of them can serve as useful. I more meant that you might see something like "$F" as a hint doesn't seem to add much to me, and that hints also lead you down a particular path first which can make it more difficult or easier to find shorter proofs. However, if you just want a faster proof, then using all of the suggested hints probably comes as the way to go.

Q4: Hints do NOT need to come as deducible from the axioms.

Q5: Hints can contradict the axioms, sure.

The manual says "A derived clause matches a hint if it subsumes the hint.

...

In short, the default value of the hints_part parameter says to select clauses that match hints (lightest first) whenever any are available."

"Clause C subsumes clause D if the variables of C can be instantiated in such a way that it becomes a subclause of D. If C subsumes D, then D can be discarded, because it is weaker than or equivalent to C. (There are some proof procedures that require retention of subsumed clauses.)"

So let's say that you put

 1. x ^((y^z) V v)=x V y as a hint.

Then if Prover9 generates

 2. x ^ ((x^x) V v)=x V x

x ^ ((x^x) V v)=x V x will get selected whenever it's available, since it matches the hint.

This explanation isn't complete, because I'm not exactly sure how "subclause" gets defined.

Still, instead of generating formulas with the original axioms and whatever procedure Prover9 uses to generate formulas, formulas that match hints will get put to the front of the list for generating formulas. This can pick up the speed of the program, but from what I've read about some other problems it seems that many difficult problems basically wouldn't have gotten proved automatically if it weren't for things like hints, weighting, and other strategies.

Q6: I'm not sure which formulas you're referring to. In Prover9, of course, you can click on "show output" and look through the dozens of formulas it has generated. You could also set lemmas you think of as useful as additional goals, and then use Prooftrans to generate hints from those lemmas to use as hints on the next run. Or you could use the steps of the proofs of those lemmas as hints for the next run. There's no fallacy in terms of reasoning if you use steps of those proofs as hints, or the hints suggested by Prooftrans, because hints don't actually add any assumptions to the initial set. The hint mechanism works, at least according to my somewhat rough understanding, by changing the search procedure to use a clause that matches a hint once we have something which matches a hint (that is, the program has to deduce something that matches a hint, and only then can what matches the hint get used).