nltk.inference.prover9 module

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

class nltk.inference.prover9.Prover9CommandParent[source]

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 the list of the current assumptions.

class nltk.inference.prover9.Prover9Command[source]

Bases: nltk.inference.prover9.Prover9CommandParent, nltk.inference.api.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)[source]
  • 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)[source]

:see BaseProverCommand.decorate_proof()

class nltk.inference.prover9.Prover9Parent[source]

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.

config_prover9(binary_location, verbose=False)[source]
prover9_input(goal, assumptions)[source]

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.


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.


Convert a logic.Expression to Prover9 format.

class nltk.inference.prover9.Prover9[source]

Bases: nltk.inference.prover9.Prover9Parent, nltk.inference.api.Prover

prover9_input(goal, assumptions)[source]


exception nltk.inference.prover9.Prover9Exception[source]

Bases: Exception

__init__(returncode, message)[source]
exception nltk.inference.prover9.Prover9FatalException[source]

Bases: nltk.inference.prover9.Prover9Exception

exception nltk.inference.prover9.Prover9LimitExceededException[source]

Bases: nltk.inference.prover9.Prover9Exception


Test that parsing works OK.


Try some proofs and exhibit the results.