Package nltk :: Package inference :: Module api :: Class BaseProverCommand
[hide private]
[frames] | no frames]

type BaseProverCommand

source code

        object --+        
                 |        
TheoremToolCommand --+    
                     |    
BaseTheoremToolCommand --+
                         |
        object --+       |
                 |       |
TheoremToolCommand --+   |
                     |   |
         ProverCommand --+
                         |
                        BaseProverCommand
Known Subclasses:

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.

Instance Methods [hide private]
 
__init__(self, prover, goal=None, assumptions=None) source code
 
prove(self, verbose=False)
Perform the actual proof.
source code
 
proof(self, simplify=True)
Return the proof string
source code
 
decorate_proof(self, proof_string, simplify=True)
Modify and return the proof string
source code
 
get_prover(self)
Return the prover object
source code

Inherited from BaseTheoremToolCommand: add_assumptions, assumptions, goal, print_assumptions, retract_assumptions

Instance Variables [hide private]
  _prover
The theorem tool to execute with the assumptions

Inherited from BaseTheoremToolCommand (private): _result

Method Details [hide private]

__init__(self, prover, goal=None, assumptions=None)
(Constructor)

source code 
Parameters:
  • prover (Prover) - The theorem tool to execute with the assumptions
Overrides: BaseTheoremToolCommand.__init__

See Also: BaseTheoremToolCommand

prove(self, verbose=False)

source code 

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

Overrides: ProverCommand.prove

proof(self, simplify=True)

source code 

Return the proof string

Parameters:
  • simplify - boolean simplify the proof?
Returns:
str
Overrides: ProverCommand.proof

decorate_proof(self, proof_string, simplify=True)

source code 

Modify and return the proof string

Parameters:
  • proof_string - str the proof to decorate
  • simplify - boolean simplify the proof?
Returns:
str

get_prover(self)

source code 

Return the prover object

Returns:
Prover
Overrides: ProverCommand.get_prover
(inherited documentation)