Package nltk :: Package inference :: Module prover9 :: Class Prover9Command

type Prover9Command

                    object --+    
                             |    
          Prover9CommandParent --+
                                 |
            object --+           |
                     |           |
api.TheoremToolCommand --+       |
                         |       |
api.BaseTheoremToolCommand --+   |
                             |   |
            object --+       |   |
                     |       |   |
api.TheoremToolCommand --+   |   |
                         |   |   |
         api.ProverCommand --+   |
                             |   |
         api.BaseProverCommand --+
                                 |
                                Prover9Command

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.

Instance Methods

[hide private]

__init__(self, goal=None, assumptions=None, timeout=60, prover=None)

source code

decorate_proof(self, proof_string, simplify=True)
@see BaseProverCommand.decorate_proof()

source code

Inherited from Prover9CommandParent: print_assumptions

Inherited from api.BaseProverCommand: get_prover, proof, prove

Inherited from api.BaseTheoremToolCommand: add_assumptions, assumptions, goal, retract_assumptions

Instance Variables

[hide private]

Inherited from api.BaseProverCommand (private): _prover

Inherited from api.BaseTheoremToolCommand (private): _result

Method Details

[hide private]

init(self, goal=None, assumptions=None, timeout=60, prover=None)
(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.
timeout (int) - number of seconds before timeout; set to 0 for no timeout.
prover (Prover9) - a prover. If not set, one will be created.

Overrides: api.BaseTheoremToolCommand.__init__

decorate_proof(self, proof_string, simplify=True)

source code

@see BaseProverCommand.decorate_proof()

Parameters:

proof_string - str the proof to decorate
simplify - boolean simplify the proof?

Returns:

str

Overrides: api.BaseProverCommand.decorate_proof

type Prover9Command

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

decorate_proof(self, proof_string, simplify=True)

init(self, goal=None, assumptions=None, timeout=60, prover=None)
(Constructor)