class documentation
class TableauProverCommand(BaseProverCommand): (source)
Constructor: TableauProverCommand(goal, assumptions, prover)
Undocumented
Method | __init__ |
No summary |
Inherited from BaseProverCommand
:
Method | decorate |
Modify and return the proof string :param proof_string: str the proof to decorate :param simplify: bool simplify the proof? :return: str |
Method | get |
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. Store the result to prevent unnecessary re-proving. |
Instance Variable | _proof |
Undocumented |
Instance Variable | _prover |
The theorem tool to execute with the assumptions |
Instance Variable | _result |
A holder for the result, to prevent unnecessary re-proving |
Inherited from BaseTheoremToolCommand
(via BaseProverCommand
):
Method | add |
Add new assumptions to the assumption list. |
Method | assumptions |
List the current assumptions. |
Method | goal |
Return the goal |
Method | print |
Print the list of the current assumptions. |
Method | retract |
Retract assumptions from the assumption list. |
Instance Variable | _assumptions |
Undocumented |
Instance Variable | _goal |
Undocumented |