nltk.ParallelProverBuilderCommand
¶
-
class
nltk.
ParallelProverBuilderCommand
(prover, modelbuilder, goal=None, assumptions=None)[source]¶ 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”.
Methods¶
__init__ (prover, modelbuilder[, goal, ...]) |
|
add_assumptions (new_assumptions) |
Add new assumptions to the assumption list. |
assumptions () |
List the current assumptions. |
build_model ([verbose]) |
|
decorate_proof (proof_string[, simplify]) |
Modify and return the proof string |
get_model_builder () |
|
get_prover () |
|
goal () |
Return the goal |
model ([format]) |
Return a string representation of the model |
print_assumptions () |
Print the list of the current assumptions. |
proof ([simplify]) |
Return the proof string |
prove ([verbose]) |
|
retract_assumptions (retracted[, debug]) |
Retract assumptions from the assumption list. |