nltk.inference.resolution.ResolutionProverCommand

class documentation

class ResolutionProverCommand(BaseProverCommand): (source)

Undocumented

Method	`__init__`	No summary
Method	`find_answers`	Undocumented
Method	`prove`	Perform the actual proof. Store the result to prevent unnecessary re-proving.
Static Method	`_decorate_clauses`	Decorate the proof output.
Instance Variable	`_clauses`	Undocumented
Instance Variable	`_proof`	Undocumented
Instance Variable	`_result`	A holder for the result, to prevent unnecessary re-proving

Inherited from BaseProverCommand:

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
Instance Variable	`_prover`	The theorem tool to execute with the assumptions

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, goal=None, assumptions=None, prover=None): (source) ¶

overrides nltk.inference.api.BaseProverCommand.__init__

Parameters
goal:sem.Expression	Input expression to prove
assumptions:list(sem.Expression)	Input expressions to use as assumptions in the proof.
prover	Undocumented

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

Undocumented

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

overrides nltk.inference.api.BaseProverCommand.prove

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

@staticmethod
def _decorate_clauses(clauses): (source) ¶

Decorate the proof output.

Undocumented

overrides nltk.inference.api.BaseProverCommand._proof

Undocumented

overrides nltk.inference.api.BaseProverCommand._result

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