nltk.inference.ParallelProverBuilderCommand¶
- class nltk.inference.ParallelProverBuilderCommand[source]¶
Bases:
BaseProverCommand
,BaseModelBuilderCommand
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”.
- __init__(prover, modelbuilder, goal=None, assumptions=None)[source]¶
- Parameters
prover (Prover) – The theorem tool to execute with the assumptions
- See
BaseTheoremToolCommand
- prove(verbose=False)[source]¶
Perform the actual proof. Store the result to prevent unnecessary re-proving.
- build_model(verbose=False)[source]¶
Attempt to build a model. Store the result to prevent unnecessary re-building.
- add_assumptions(new_assumptions)[source]¶
Add new assumptions to the assumption list.
- Parameters
new_assumptions (list(sem.Expression)) – new assumptions
- decorate_proof(proof_string, simplify=True)[source]¶
Modify and return the proof string :param proof_string: str the proof to decorate :param simplify: bool simplify the proof? :return: str
- model(format=None)[source]¶
Return a string representation of the model
- Parameters
simplify – bool simplify the proof?
- Returns
str
- proof(simplify=True)[source]¶
Return the proof string :param simplify: bool simplify the proof? :return: str
- retract_assumptions(retracted, debug=False)[source]¶
Retract assumptions from the assumption list.
- Parameters
debug (bool) – If True, give warning when
retracted
is not present on assumptions list.retracted (list(sem.Expression)) – assumptions to be retracted