nltk.inference.prover9

module documentation
(source)

A theorem prover that makes use of the external 'Prover9' package.

Class Prover9 No class docstring; 1/3 instance variable, 4/5 methods documented
Class 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.
Class Prover9CommandParent A common base class used by both Prover9Command and MaceCommand, which is responsible for maintaining a goal and a set of assumptions, and generating prover9-style input files from them.
Class Prover9Parent A common class extended by both Prover9 and Mace <mace.Mace>. It contains the functionality required to convert NLTK-style expressions into Prover9-style expressions.
Exception Prover9Exception Undocumented
Exception Prover9FatalException Undocumented
Exception Prover9LimitExceededException Undocumented
Function convert_to_prover9 Convert a logic.Expression to Prover9 format.
Function demo Undocumented
Function spacer Undocumented
Function test_config Undocumented
Function test_convert_to_prover9 Test that parsing works OK.
Function test_prove Try some proofs and exhibit the results.
Variable arguments Undocumented
Variable expressions Undocumented
Variable p9_return_codes Undocumented
Function _convert_to_prover9 Convert logic.Expression to Prover9 formatted string.
def convert_to_prover9(input): (source)

Convert a logic.Expression to Prover9 format.

def demo(): (source)

Undocumented

def spacer(num=45): (source)

Undocumented

def test_config(): (source)

Undocumented

def test_convert_to_prover9(expr): (source)

Test that parsing works OK.

def test_prove(arguments): (source)

Try some proofs and exhibit the results.

arguments: list[tuple] = (source)

Undocumented

expressions: list[str] = (source)

Undocumented

p9_return_codes: dict = (source)

Undocumented

def _convert_to_prover9(expression): (source)

Convert logic.Expression to Prover9 formatted string.