nltk.ResolutionProverCommand

class nltk.ResolutionProverCommand(goal=None, assumptions=None, prover=None)[source]

Methods

__init__([goal, assumptions, 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]) Modify and return the proof string
find_answers([verbose])
get_prover()
goal() Return the goal
print_assumptions() 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.