nltk.inference.prover9.Prover9Command

class documentation

class Prover9Command(Prover9CommandParent, BaseProverCommand): (source)

Constructor: Prover9Command(goal, assumptions, timeout, prover)

View In Hierarchy

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.

Method __init__ No summary
Method decorate_proof :see BaseProverCommand.decorate_proof()

Inherited from Prover9CommandParent:

Method print_assumptions Print the list of the current assumptions.

Inherited from BaseProverCommand (via Prover9CommandParent):

Method get_prover Return the prover object :return: Prover
Method proof Return the proof string :param simplify: bool simplify the proof? :return: str
Method prove Perform the actual proof. Store the result to prevent unnecessary re-proving.
Instance Variable _proof Undocumented
Instance Variable _prover The theorem tool to execute with the assumptions
Instance Variable _result A holder for the result, to prevent unnecessary re-proving

Inherited from BaseTheoremToolCommand (via Prover9CommandParent, BaseProverCommand):

Method add_assumptions Add new assumptions to the assumption list.
Method assumptions List the current assumptions.
Method goal Return the goal
Method retract_assumptions Retract assumptions from the assumption list.
Instance Variable _assumptions Undocumented
Instance Variable _goal Undocumented
def __init__(self, goal=None, assumptions=None, timeout=60, prover=None): (source)
overrides nltk.inference.api.BaseProverCommand.__init__
Parameters
goal:sem.ExpressionInput expression to prove
assumptions:list(sem.Expression)Input expressions to use as assumptions in the proof.
timeout:intnumber of seconds before timeout; set to 0 for no timeout.
prover:Prover9a prover. If not set, one will be created.
def decorate_proof(self, proof_string, simplify=True): (source)
overrides nltk.inference.api.BaseProverCommand.decorate_proof

:see BaseProverCommand.decorate_proof()