nltk.inference.TableauProverCommand

class nltk.inference.TableauProverCommand

Bases: BaseProverCommand

__init__(goal=None, assumptions=None, prover=None)

Parameters

• goal (sem.Expression) – Input expression to prove

• assumptions (list(sem.Expression)) – Input expressions to use as assumptions in the proof.

add_assumptions(new_assumptions)

Add new assumptions to the assumption list.

Parameters

new_assumptions (list(sem.Expression)) – new assumptions

assumptions()

List the current assumptions.

Returns

list of Expression

decorate_proof(proof_string, simplify=True)

Modify and return the proof string :param proof_string: str the proof to decorate :param simplify: bool simplify the proof? :return: str

get_prover()

Return the prover object :return: Prover

goal()

Return the goal

Returns

Expression

print_assumptions()

Print the list of the current assumptions.

proof(simplify=True)

Return the proof string :param simplify: bool simplify the proof? :return: str

prove(verbose=False)

Perform the actual proof. Store the result to prevent unnecessary re-proving.

retract_assumptions(retracted, debug=False)

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