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.BaseModelBuilderCommand

Bases: BaseTheoremToolCommand, 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)

Parameters:

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

See:

BaseTheoremToolCommand

build_model(verbose=False)

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

get_model_builder()

Return the model builder object :return: ModelBuilder

model(format=None)

Return a string representation of the model

Parameters:

simplify – bool simplify the proof?

Returns:

str

class nltk.inference.api.BaseProverCommand

Bases: BaseTheoremToolCommand, 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)

Parameters:

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

See:

BaseTheoremToolCommand

decorate_proof(proof_string, simplify=True)

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

get_prover()

Return the prover object :return: Prover

proof(simplify=True)

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

prove(verbose=False)

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

class nltk.inference.api.BaseTheoremToolCommand

Bases: TheoremToolCommand

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

__init__(goal=None, assumptions=None)

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)

Add new assumptions to the assumption list.

Parameters:

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

assumptions()

List the current assumptions.

Returns:

list of Expression

goal()

Return the goal

Returns:

Expression

print_assumptions()

Print the list of the current assumptions.

retract_assumptions(retracted, debug=False)

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

class nltk.inference.api.ModelBuilder

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)

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

class nltk.inference.api.ModelBuilderCommand

Bases: 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)

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

abstract get_model_builder()

Return the model builder object :return: ModelBuilder

abstract model(format=None)

Return a string representation of the model

Parameters:

simplify – bool simplify the proof?

Returns:

str

class nltk.inference.api.ModelBuilderCommandDecorator

Bases: TheoremToolCommandDecorator, ModelBuilderCommand

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

__init__(modelBuilderCommand)

Parameters:

modelBuilderCommand – ModelBuilderCommand to decorate

build_model(verbose=False)

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

get_model_builder()

Return the model builder object :return: ModelBuilder

model(format=None)

Return a string representation of the model

Parameters:

simplify – bool simplify the proof?

Returns:

str

class nltk.inference.api.ParallelProverBuilder

Bases: Prover, 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)

class nltk.inference.api.ParallelProverBuilderCommand

Bases: BaseProverCommand, 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)

Parameters:

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

See:

BaseTheoremToolCommand

build_model(verbose=False)

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

prove(verbose=False)

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

class nltk.inference.api.Prover

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)

Returns:

Whether the proof was successful or not.

Return type:

bool

class nltk.inference.api.ProverCommand

Bases: 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 get_prover()

Return the prover object :return: Prover

abstract proof(simplify=True)

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

abstract prove(verbose=False)

Perform the actual proof.

class nltk.inference.api.ProverCommandDecorator

Bases: TheoremToolCommandDecorator, ProverCommand

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

__init__(proverCommand)

Parameters:

proverCommand – ProverCommand to decorate

decorate_proof(proof_string, simplify=True)

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

get_prover()

Return the prover object :return: Prover

proof(simplify=True)

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

prove(verbose=False)

Perform the actual proof.

class nltk.inference.api.TheoremToolCommand

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)

Add new assumptions to the assumption list.

Parameters:

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

abstract assumptions()

List the current assumptions.

Returns:

list of Expression

abstract goal()

Return the goal

Returns:

Expression

abstract print_assumptions()

Print the list of the current assumptions.

abstract retract_assumptions(retracted, debug=False)

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

class nltk.inference.api.TheoremToolCommandDecorator

Bases: TheoremToolCommand

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

__init__(command)

Parameters:

command – TheoremToolCommand to decorate

add_assumptions(new_assumptions)

Add new assumptions to the assumption list.

Parameters:

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

assumptions()

List the current assumptions.

Returns:

list of Expression

goal()

Return the goal

Returns:

Expression

print_assumptions()

Print the list of the current assumptions.

retract_assumptions(retracted, debug=False)

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

class nltk.inference.api.TheoremToolThread

Bases: Thread

__init__(command, verbose, name=None)

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 a list or tuple of arguments 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.

property result

run()

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.