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

Class Prover9Command

                object --+    
                         |    
      Prover9CommandParent --+
                             |
            object --+       |
                     |       |
api.TheoremToolCommand --+   |
                         |   |
         api.ProverCommand --+
                             |
                            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=[], timeout=60) source code

show_proof(self, simplify=True)
Print out a Prover9 proof.

source code

Inherited from Prover9CommandParent: print_assumptions

Inherited from api.ProverCommand: get_prover, prove

Inherited from api.TheoremToolCommand: add_assumptions, assumptions, goal, 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=`[]`, timeout=60)
(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.

Overrides: api.ProverCommand.__init__

show_proof(self, simplify=True)

source code

Print out a Prover9 proof.

Parameters:

simplify (bool) - if True, simplify the output file using Prover9's prooftrans.

Overrides: api.ProverCommand.show_proof

Class Prover9Command

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

show_proof(self, simplify=True)

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