nltk.inference.prover9 module

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

class nltk.inference.prover9.Prover9

Bases: Prover9Parent, Prover

__init__(timeout=60)

prover9_input(goal, assumptions)

See:

Prover9Parent.prover9_input

class nltk.inference.prover9.Prover9Command

Bases: Prover9CommandParent, BaseProverCommand

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.

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

Parameters:

• goal (sem.Expression) – Input expression to prove

• assumptions (list(sem.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.

decorate_proof(proof_string, simplify=True)

:see BaseProverCommand.decorate_proof()

class nltk.inference.prover9.Prover9CommandParent

Bases: object

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.

print_assumptions(output_format='nltk')

Print the list of the current assumptions.

exception nltk.inference.prover9.Prover9Exception

Bases: Exception

__init__(returncode, message)

exception nltk.inference.prover9.Prover9FatalException

Bases: Prover9Exception

exception nltk.inference.prover9.Prover9LimitExceededException

Bases: Prover9Exception

class nltk.inference.prover9.Prover9Parent

Bases: object

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.

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.

config_prover9(binary_location, verbose=False)

prover9_input(goal, assumptions)

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.

nltk.inference.prover9.convert_to_prover9(input)

Convert a logic.Expression to Prover9 format.

nltk.inference.prover9.demo()

nltk.inference.prover9.spacer(num=45)

nltk.inference.prover9.test_config()

nltk.inference.prover9.test_convert_to_prover9(expr)

Test that parsing works OK.

nltk.inference.prover9.test_prove(arguments)

Try some proofs and exhibit the results.