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

assumptions()[source]

List the current assumptions.

Returns

list of Expression

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

get_model_builder()[source]

Return the model builder object :return: ModelBuilder

get_prover()[source]

Return the prover object :return: Prover

goal()[source]

Return the goal

Returns

Expression

model(format=None)[source]

Return a string representation of the model

Parameters

simplify – bool simplify the proof?

Returns

str

print_assumptions()[source]

Print the list of the current assumptions.

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