Package nltk :: Package inference :: Module resolution :: Class ResolutionCommand

Class ResolutionCommand

            object --+        
                     |        
api.TheoremToolCommand --+    
                         |    
         api.ProverCommand --+
                             |
                            ResolutionCommand

Instance Methods

[hide private]

__init__(self, goal=None, assumptions=[]) source code

prove(self, verbose=False)
Perform the actual proof.

source code

find_answers(self, verbose=False)

source code

decorate_proof(self, clauses)
Decorate the proof output.

source code

Inherited from api.ProverCommand: get_prover, show_proof

Inherited from api.TheoremToolCommand: add_assumptions, assumptions, goal, print_assumptions, retract_assumptions

Inherited from object: __delattr__, __getattribute__, __hash__, __new__, __reduce__, __reduce_ex__, __repr__, __setattr__, __str__

Instance Variables

[hide private]

Inherited from api.ProverCommand (private): _prover

Inherited from api.TheoremToolCommand (private): _assumptions, _goal, _result

Properties

[hide private]

Inherited from object: __class__

Method Details

[hide private]

init(self, goal=None, assumptions=`[]`)
(Constructor)

source code

Parameters:

goal (logic.Expression) - Input expression to prove
assumptions (list of logic.Expression) - Input expressions to use as assumptions in the proof.

Overrides: api.ProverCommand.__init__

prove(self, verbose=False)

source code

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

Overrides: api.ProverCommand.prove

Class ResolutionCommand

__init__(self, goal=None, assumptions=[]) (Constructor)

prove(self, verbose=False)

init(self, goal=None, assumptions=`[]`)
(Constructor)