nltk.inference.api module

Interfaces and base classes for theorem provers and model builders.

Prover is a standard interface for a theorem prover which tries to prove a goal from a list of assumptions.

ModelBuilder is a standard interface for a model builder. Given just a set of assumptions. the model builder tries to build a model for the assumptions. Given a set of assumptions and a goal G, the model builder tries to find a counter-model, in the sense of a model that will satisfy the assumptions plus the negation of G.

class nltk.inference.api.Prover[source]

Bases: object

Interface for trying to prove a goal from assumptions. Both the goal and the assumptions are constrained to be formulas of logic.Expression.

prove(goal=None, assumptions=None, verbose=False)[source]
Returns

Whether the proof was successful or not.

Return type

bool

class nltk.inference.api.ModelBuilder[source]

Bases: object

Interface for trying to build a model of set of formulas. Open formulas are assumed to be universally quantified. Both the goal and the assumptions are constrained to be formulas of logic.Expression.

build_model(goal=None, assumptions=None, verbose=False)[source]

Perform the actual model building. :return: Whether a model was generated :rtype: bool

class nltk.inference.api.TheoremToolCommand[source]

Bases: object

This class holds a goal and a list of assumptions to be used in proving or model building.

abstract add_assumptions(new_assumptions)[source]

Add new assumptions to the assumption list.

Parameters

new_assumptions (list(sem.Expression)) – new assumptions

abstract retract_assumptions(retracted, debug=False)[source]

Retract assumptions from the assumption list.

Parameters
  • debug (bool) – If True, give warning when retracted is not present on assumptions list.

  • retracted (list(sem.Expression)) – assumptions to be retracted

abstract assumptions()[source]

List the current assumptions.

Returns

list of Expression

abstract goal()[source]

Return the goal

Returns

Expression

abstract print_assumptions()[source]

Print the list of the current assumptions.

class nltk.inference.api.ProverCommand[source]

Bases: nltk.inference.api.TheoremToolCommand

This class holds a Prover, a goal, and a list of assumptions. When prove() is called, the Prover is executed with the goal and assumptions.

abstract prove(verbose=False)[source]

Perform the actual proof.

abstract proof(simplify=True)[source]

Return the proof string :param simplify: bool simplify the proof? :return: str

abstract get_prover()[source]

Return the prover object :return: Prover

class nltk.inference.api.ModelBuilderCommand[source]

Bases: nltk.inference.api.TheoremToolCommand

This class holds a ModelBuilder, a goal, and a list of assumptions. When build_model() is called, the ModelBuilder is executed with the goal and assumptions.

abstract build_model(verbose=False)[source]

Perform the actual model building. :return: A model if one is generated; None otherwise. :rtype: sem.Valuation

abstract model(format=None)[source]

Return a string representation of the model

Parameters

simplify – bool simplify the proof?

Returns

str

abstract get_model_builder()[source]

Return the model builder object :return: ModelBuilder

class nltk.inference.api.BaseTheoremToolCommand[source]

Bases: nltk.inference.api.TheoremToolCommand

This class holds a goal and a list of assumptions to be used in proving or model building.

__init__(goal=None, assumptions=None)[source]
Parameters
  • goal (sem.Expression) – Input expression to prove

  • assumptions (list(sem.Expression)) – Input expressions to use as assumptions in the proof.

add_assumptions(new_assumptions)[source]

Add new assumptions to the assumption list.

Parameters

new_assumptions (list(sem.Expression)) – new assumptions

retract_assumptions(retracted, debug=False)[source]

Retract assumptions from the assumption list.

Parameters
  • debug (bool) – If True, give warning when retracted is not present on assumptions list.

  • retracted (list(sem.Expression)) – assumptions to be retracted

assumptions()[source]

List the current assumptions.

Returns

list of Expression

goal()[source]

Return the goal

Returns

Expression

print_assumptions()[source]

Print the list of the current assumptions.

class nltk.inference.api.BaseProverCommand[source]

Bases: nltk.inference.api.BaseTheoremToolCommand, nltk.inference.api.ProverCommand

This class holds a Prover, a goal, and a list of assumptions. When prove() is called, the Prover is executed with the goal and assumptions.

__init__(prover, goal=None, assumptions=None)[source]
Parameters

prover (Prover) – The theorem tool to execute with the assumptions

See

BaseTheoremToolCommand

prove(verbose=False)[source]

Perform the actual proof. Store the result to prevent unnecessary re-proving.

proof(simplify=True)[source]

Return the proof string :param simplify: bool simplify the proof? :return: str

decorate_proof(proof_string, simplify=True)[source]

Modify and return the proof string :param proof_string: str the proof to decorate :param simplify: bool simplify the proof? :return: str

get_prover()[source]

Return the prover object :return: Prover

class nltk.inference.api.BaseModelBuilderCommand[source]

Bases: nltk.inference.api.BaseTheoremToolCommand, nltk.inference.api.ModelBuilderCommand

This class holds a ModelBuilder, a goal, and a list of assumptions. When build_model() is called, the ModelBuilder is executed with the goal and assumptions.

__init__(modelbuilder, goal=None, assumptions=None)[source]
Parameters

modelbuilder (ModelBuilder) – The theorem tool to execute with the assumptions

See

BaseTheoremToolCommand

build_model(verbose=False)[source]

Attempt to build a model. Store the result to prevent unnecessary re-building.

model(format=None)[source]

Return a string representation of the model

Parameters

simplify – bool simplify the proof?

Returns

str

get_model_builder()[source]

Return the model builder object :return: ModelBuilder

class nltk.inference.api.TheoremToolCommandDecorator[source]

Bases: nltk.inference.api.TheoremToolCommand

A base decorator for the ProverCommandDecorator and ModelBuilderCommandDecorator classes from which decorators can extend.

__init__(command)[source]
Parameters

commandTheoremToolCommand to decorate

assumptions()[source]

List the current assumptions.

Returns

list of Expression

goal()[source]

Return the goal

Returns

Expression

add_assumptions(new_assumptions)[source]

Add new assumptions to the assumption list.

Parameters

new_assumptions (list(sem.Expression)) – new assumptions

retract_assumptions(retracted, debug=False)[source]

Retract assumptions from the assumption list.

Parameters
  • debug (bool) – If True, give warning when retracted is not present on assumptions list.

  • retracted (list(sem.Expression)) – assumptions to be retracted

print_assumptions()[source]

Print the list of the current assumptions.

class nltk.inference.api.ProverCommandDecorator[source]

Bases: nltk.inference.api.TheoremToolCommandDecorator, nltk.inference.api.ProverCommand

A base decorator for the ProverCommand class from which other prover command decorators can extend.

__init__(proverCommand)[source]
Parameters

proverCommandProverCommand to decorate

prove(verbose=False)[source]

Perform the actual proof.

proof(simplify=True)[source]

Return the proof string :param simplify: bool simplify the proof? :return: str

decorate_proof(proof_string, simplify=True)[source]

Modify and return the proof string :param proof_string: str the proof to decorate :param simplify: bool simplify the proof? :return: str

get_prover()[source]

Return the prover object :return: Prover

class nltk.inference.api.ModelBuilderCommandDecorator[source]

Bases: nltk.inference.api.TheoremToolCommandDecorator, nltk.inference.api.ModelBuilderCommand

A base decorator for the ModelBuilderCommand class from which other prover command decorators can extend.

__init__(modelBuilderCommand)[source]
Parameters

modelBuilderCommandModelBuilderCommand to decorate

build_model(verbose=False)[source]

Attempt to build a model. Store the result to prevent unnecessary re-building.

model(format=None)[source]

Return a string representation of the model

Parameters

simplify – bool simplify the proof?

Returns

str

get_model_builder()[source]

Return the model builder object :return: ModelBuilder

class nltk.inference.api.ParallelProverBuilder[source]

Bases: nltk.inference.api.Prover, nltk.inference.api.ModelBuilder

This class stores both a prover and a model builder and when either prove() or build_model() is called, then both theorem tools are run in parallel. Whichever finishes first, the prover or the model builder, is the result that will be used.

__init__(prover, modelbuilder)[source]
class nltk.inference.api.ParallelProverBuilderCommand[source]

Bases: nltk.inference.api.BaseProverCommand, nltk.inference.api.BaseModelBuilderCommand

This command stores both a prover and a model builder and when either prove() or build_model() is called, then both theorem tools are run in parallel. Whichever finishes first, the prover or the model builder, is the result that will be used.

Because the theorem prover result is the opposite of the model builder result, we will treat self._result as meaning “proof found/no model found”.

__init__(prover, modelbuilder, goal=None, assumptions=None)[source]
Parameters

prover (Prover) – The theorem tool to execute with the assumptions

See

BaseTheoremToolCommand

prove(verbose=False)[source]

Perform the actual proof. Store the result to prevent unnecessary re-proving.

build_model(verbose=False)[source]

Attempt to build a model. Store the result to prevent unnecessary re-building.

class nltk.inference.api.TheoremToolThread[source]

Bases: threading.Thread

__init__(command, verbose, name=None)[source]

This constructor should always be called with keyword arguments. Arguments are:

group should be None; reserved for future extension when a ThreadGroup class is implemented.

target is the callable object to be invoked by the run() method. Defaults to None, meaning nothing is called.

name is the thread name. By default, a unique name is constructed of the form “Thread-N” where N is a small decimal number.

args is the argument tuple for the target invocation. Defaults to ().

kwargs is a dictionary of keyword arguments for the target invocation. Defaults to {}.

If a subclass overrides the constructor, it must make sure to invoke the base class constructor (Thread.__init__()) before doing anything else to the thread.

run()[source]

Method representing the thread’s activity.

You may override this method in a subclass. The standard run() method invokes the callable object passed to the object’s constructor as the target argument, if any, with sequential and keyword arguments taken from the args and kwargs arguments, respectively.

property result