class documentation

This command stores both a prover and a model builder and when either prove() or build_model() is called, then both theorem tools are run in parallel. Whichever finishes first, the prover or the model builder, is the result that will be used.

Because the theorem prover result is the opposite of the model builder result, we will treat self._result as meaning "proof found/no model found".

Method __init__ No summary
Method build_model Attempt to build a model. Store the result to prevent unnecessary re-building.
Method prove Perform the actual proof. Store the result to prevent unnecessary re-proving.
Method _run Undocumented
Instance Variable _result A holder for the result, to prevent unnecessary re-proving

Inherited from BaseProverCommand:

Method decorate_proof Modify and return the proof string :param proof_string: str the proof to decorate :param simplify: bool simplify the proof? :return: str
Method get_prover Return the prover object :return: Prover
Method proof Return the proof string :param simplify: bool simplify the proof? :return: str
Instance Variable _proof Undocumented
Instance Variable _prover The theorem tool to execute with the assumptions

Inherited from BaseModelBuilderCommand (via BaseProverCommand):

Method get_model_builder Return the model builder object :return: ModelBuilder
Method model Return a string representation of the model
Method _decorate_model No summary
Instance Variable _model Undocumented
Instance Variable _modelbuilder The theorem tool to execute with the assumptions

Inherited from BaseTheoremToolCommand (via BaseProverCommand, BaseModelBuilderCommand):

Method add_assumptions Add new assumptions to the assumption list.
Method assumptions List the current assumptions.
Method goal Return the goal
Method print_assumptions Print the list of the current assumptions.
Method retract_assumptions Retract assumptions from the assumption list.
Instance Variable _assumptions Undocumented
Instance Variable _goal Undocumented
def __init__(self, prover, modelbuilder, goal=None, assumptions=None): (source)
Parameters
prover:ProverThe theorem tool to execute with the assumptions
modelbuilderUndocumented
goalUndocumented
assumptionsUndocumented
See Also
BaseTheoremToolCommand
def build_model(self, verbose=False): (source)

Attempt to build a model. Store the result to prevent unnecessary re-building.

def prove(self, verbose=False): (source)

Perform the actual proof. Store the result to prevent unnecessary re-proving.

def _run(self, verbose): (source)

Undocumented

A holder for the result, to prevent unnecessary re-proving