nltk.inference.Prover9Command

class nltk.inference.Prover9Command

Bases: Prover9CommandParent, BaseProverCommand

A ProverCommand specific to the Prover9 prover. It contains the a print_assumptions() method that is used to print the list of assumptions in multiple formats.

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

Parameters

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

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

• timeout (int) – number of seconds before timeout; set to 0 for no timeout.

• prover (Prover9) – a prover. If not set, one will be created.

decorate_proof(proof_string, simplify=True)

:see BaseProverCommand.decorate_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

get_prover()

Return the prover object :return: Prover

goal()

Return the goal

Returns

Expression

print_assumptions(output_format='nltk')

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