class documentation

This class holds a Prover, a goal, and a list of assumptions. When prove() is called, the Prover is executed with the goal and assumptions.

Method get_prover Return the prover object :return: Prover
Method proof Return the proof string :param simplify: bool simplify the proof? :return: str
Method prove Perform the actual proof.

Inherited from TheoremToolCommand:

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.
@abstractmethod
def get_prover(self): (source)

Return the prover object :return: Prover

@abstractmethod
def proof(self, simplify=True): (source)

Return the proof string :param simplify: bool simplify the proof? :return: str

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