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
.
- 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
.
- 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
- 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, theProver
is executed with the goal and assumptions.
- 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, theModelBuilder
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
- 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
- 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, theProver
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
- 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, theModelBuilder
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.
- class nltk.inference.api.TheoremToolCommandDecorator[source]¶
Bases:
nltk.inference.api.TheoremToolCommand
A base decorator for the
ProverCommandDecorator
andModelBuilderCommandDecorator
classes from which decorators can extend.- add_assumptions(new_assumptions)[source]¶
Add new assumptions to the assumption list.
- Parameters
new_assumptions (list(sem.Expression)) – new 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.- proof(simplify=True)[source]¶
Return the proof string :param simplify: bool simplify the proof? :return: str
- 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
modelBuilderCommand –
ModelBuilderCommand
to decorate
- build_model(verbose=False)[source]¶
Attempt to build a model. Store the result to prevent unnecessary re-building.
- 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.
- 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
- 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¶