run(ProofEnvironment env) starts a proof attempt
Parameters: env - the ProofEnvironment to which the proof object will be registered true if the proof attempt terminated normally (i.e.
setUseDecisionProcedure(boolean useDecisionProcedures) if activated the proof starter will run decision procedures on all open goals
after the normal proof search has stopped.
adds a progress monitor to the proof starter. The progress monitor will
be informed about the progress when performing a proof search. Therefore
its
ProgressMonitor.setMaximum(int) will be called handing over the
maximal number of rule steps to be performed before the proof attempt is stopped.
After each rule application the monitor will receive a call to
ProgressMonitor.setProgress(int) Parameters: pm - the ProgressMonitor to be added
initializes the proof starter, i.e. the proof is created and set up
Parameters: po - the ProofOblInput with the proof (proof attempt is onlystarted on the first proof)
starts a proof attempt
Parameters: env - the ProofEnvironment to which the proof object will be registered true if the proof attempt terminated normally (i.e. no error has occured).In particular true does not mean that the proof has been closed.
sets the maximal amount of steps to be performed
Parameters: maxSteps - the int limiting the maximal amount of steps done inautomatic proof mode throws: an - IllegalArgumentException if maxSteps is lesserthan zero
sets the strategy to be used for the prove attempt
Parameters: strategy - the Strategy to use
setUseDecisionProcedure
public void setUseDecisionProcedure(boolean useDecisionProcedures)(Code)
if activated the proof starter will run decision procedures on all open goals
after the normal proof search has stopped.
Parameters: useDecisionProcedures - the boolean if true activates otherwise disables running the decision procedures