nltk.inference.api.BaseProverCommand

class documentation

class BaseProverCommand(BaseTheoremToolCommand, ProverCommand): (source)

Known subclasses: nltk.inference.api.ParallelProverBuilderCommand, nltk.inference.prover9.Prover9Command, nltk.inference.resolution.ResolutionProverCommand, nltk.inference.tableau.TableauProverCommand

Constructor: BaseProverCommand(prover, goal, assumptions)

View In Hierarchy

This class holds a Prover, a goal, and a list of assumptions. When prove() is called, the Prover is executed with the goal and assumptions.

Method	`__init__`	No summary
Method	`decorate_proof`	Modify and return the proof string :param proof_string: str the proof to decorate :param simplify: bool simplify the proof? :return: str
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:

Method	`add_assumptions`	Add new assumptions to the assumption list.
Method	`assumptions`	List the current assumptions.
Method	`goal`	Return the goal
Method	`print_assumptions`	Print the list of the current assumptions.
Method	`retract_assumptions`	Retract assumptions from the assumption list.
Instance Variable	`_assumptions`	Undocumented
Instance Variable	`_goal`	Undocumented

def __init__(self, prover, goal=None, assumptions=None): (source) ¶

overrides nltk.inference.api.BaseTheoremToolCommand.__init__

overridden in nltk.inference.api.ParallelProverBuilderCommand, nltk.inference.prover9.Prover9Command, nltk.inference.resolution.ResolutionProverCommand, nltk.inference.tableau.TableauProverCommand

Parameters
prover:Prover	The theorem tool to execute with the assumptions
goal	Undocumented
assumptions	Undocumented
See Also
`BaseTheoremToolCommand`

def decorate_proof(self, proof_string, simplify=True): (source) ¶

overridden in nltk.inference.prover9.Prover9Command

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

def get_prover(self): (source) ¶

overrides nltk.inference.api.ProverCommand.get_prover

Return the prover object :return: Prover

def proof(self, simplify=True): (source) ¶

overrides nltk.inference.api.ProverCommand.proof

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

def prove(self, verbose=False): (source) ¶

overrides nltk.inference.api.ProverCommand.prove

overridden in nltk.inference.api.ParallelProverBuilderCommand, nltk.inference.resolution.ResolutionProverCommand

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

_proof = (source) ¶

overridden in nltk.inference.resolution.ResolutionProverCommand

Undocumented

_prover = (source) ¶

The theorem tool to execute with the assumptions

_result = (source) ¶

overrides nltk.inference.api.BaseTheoremToolCommand._result

overridden in nltk.inference.api.ParallelProverBuilderCommand, nltk.inference.resolution.ResolutionProverCommand

A holder for the result, to prevent unnecessary re-proving