On 18 May 2009, at 23:27, Artur Oliveira Gomes wrote:


Can you tell me how can I increase the default subgoal limit when
stripping a goal?

In that proof I sent you an example, or me, the complete version
of the proof creates over 34 subgoals, then, ProofPower give me
a warning telling that the proof reached the limit, and asking
me if I want to continue, entering "y".

set_int_control("tactic_subgoal_warning", 35);

or 40 or whatever you want. However, don't set the limit much bigger than the number of subgoals yo are prepared to deal with. If you set the limit high and a tactic produces 100s or 1000s of subgoals, the subgoal package could waste a lot of your time processing those subgoals and you won't know that there are an intractable number of subgoals until it has finished.

I think it would be better if the subgoal package just told you there were lots of subgoals and then carried on trying to process them rather than output the warning - you can always interrupt it if you don't want to wait. Does anyone else have any views on this?



Proofpower mailing list

Reply via email to