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.