`nltk.Prover9Command`¶

class nltk.Prover9Command(goal=None, assumptions=None, timeout=60, prover=None)[source]¶: 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.

Methods¶

__init__([goal, assumptions, timeout, prover])

param goal:	Input expression to prove

add_assumptions(new_assumptions) Add new assumptions to the assumption list.

assumptions() List the current assumptions.

decorate_proof(proof_string[, simplify]) :see BaseProverCommand.decorate_proof()

get_prover()

goal() Return the goal

print_assumptions([output_format]) Print the list of the current assumptions.

proof([simplify]) Return the proof string

prove([verbose]) Perform the actual proof.

retract_assumptions(retracted[, debug]) Retract assumptions from the assumption list.