Package nltk :: Package inference :: Module prover9 :: Class Prover9

type Prover9

   object --+    
            |    
Prover9Parent --+
                |
   object --+   |
            |   |
   api.Prover --+
                |
               Prover9

Instance Methods

[hide private]

__init__(self, timeout=60)

source code

tuple: (bool, str)

_prove(self, goal=None, assumptions=None, verbose=False)
Use Prover9 to prove a theorem.

source code

prover9_input(self, goal, assumptions)
Returns: The input string that should be provided to the prover9 binary.

source code

_call_prover9(self, input_str, args=[], verbose=False)
Call the prover9 binary with the given input. source code

_call_prooftrans(self, input_str, args=[], verbose=False)
Call the prooftrans binary with the given input. source code

Inherited from Prover9Parent: binary_locations, config_prover9

Inherited from Prover9Parent (private): _call, _find_binary

Inherited from api.Prover: prove

Class Variables

[hide private]

_prover9_bin = None

_prooftrans_bin = None

Inherited from Prover9Parent (private): _binary_location

Instance Variables

[hide private]

_timeout
The timeout value for prover9.

Method Details

[hide private]

init(self, timeout=60)
(Constructor)

source code

Overrides: Prover9Parent.__init__

_prove(self, goal=None, assumptions=None, verbose=False)

source code

Use Prover9 to prove a theorem.

Returns: tuple: (bool, str): A pair whose first element is a boolean indicating if the proof was successful (i.e. returns value of 0) and whose second element is the output of the prover.
Overrides: api.Prover._prove

prover9_input(self, goal, assumptions)

source code

Returns:: The input string that should be provided to the prover9 binary. This string is formed based on the goal, assumptions, and timeout value of this object.
Overrides: Prover9Parent.prover9_input

See Also: Prover9Parent.prover9_input