nltk.inference.prover9.Prover9

class documentation

class Prover9(Prover9Parent, Prover): (source)

Constructor: Prover9(timeout)

Undocumented

Method	`__init__`	Undocumented
Method	`prover9_input`	No summary
Method	`_call_prooftrans`	Call the `prooftrans` binary with the given input.
Method	`_call_prover9`	Call the `prover9` binary with the given input.
Method	`_prove`	Use Prover9 to prove a theorem. :return: 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.
Instance Variable	`_prooftrans_bin`	Undocumented
Instance Variable	`_prover9_bin`	Undocumented
Instance Variable	`_timeout`	The timeout value for prover9. If a proof can not be found in this amount of time, then prover9 will return false. (Use 0 for no timeout.)

Inherited from Prover9Parent:

Method	`binary_locations`	A list of directories that should be searched for the prover9 executables. This list is used by `config_prover9` when searching for the prover9 executables.
Method	`config_prover9`	Undocumented
Method	`_call`	Call the binary with the given input.
Method	`_find_binary`	Undocumented
Instance Variable	`_binary_location`	Undocumented

Inherited from Prover (via Prover9Parent):

Method prove No summary

def __init__(self, timeout=60): (source) ¶

Undocumented

def prover9_input(self, goal, assumptions): (source) ¶

overrides nltk.inference.prover9.Prover9Parent.prover9_input

See Also
Prover9Parent.prover9_input

def _call_prooftrans(self, input_str, args=[], verbose=False): (source) ¶

Call the prooftrans binary with the given input.

Parameters
input_str	A string whose contents are used as stdin.
args	A list of command-line arguments.
verbose	Undocumented
Returns
A tuple (stdout, returncode)
See Also
`config_prover9`

def _call_prover9(self, input_str, args=[], verbose=False): (source) ¶

Call the prover9 binary with the given input.

Parameters
input_str	A string whose contents are used as stdin.
args	A list of command-line arguments.
verbose	Undocumented
Returns
A tuple (stdout, returncode)
See Also
`config_prover9`

def _prove(self, goal=None, assumptions=None, verbose=False): (source) ¶

overrides nltk.inference.api.Prover._prove

Use Prover9 to prove a theorem. :return: 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.

_prooftrans_bin = (source) ¶

Undocumented

_prover9_bin = (source) ¶

overrides nltk.inference.prover9.Prover9Parent._prover9_bin

Undocumented

_timeout = (source) ¶

The timeout value for prover9. If a proof can not be found in this amount of time, then prover9 will return false. (Use 0 for no timeout.)