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[source]¶
Bases:
BaseTheoremToolCommand
,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
- class nltk.inference.api.BaseProverCommand[source]¶
Bases:
BaseTheoremToolCommand
,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
- 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
- class nltk.inference.api.BaseTheoremToolCommand[source]¶
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)[source]¶
- Parameters:
goal (sem.Expression) – Input expression to prove
assumptions (list(sem.Expression)) – Input expressions to use as assumptions in the proof.
- 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.ModelBuilderCommand[source]¶
Bases:
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.
- class nltk.inference.api.ModelBuilderCommandDecorator[source]¶
Bases:
TheoremToolCommandDecorator
,ModelBuilderCommand
A base decorator for the
ModelBuilderCommand
class from which other prover command decorators can extend.- __init__(modelBuilderCommand)[source]¶
- Parameters:
modelBuilderCommand –
ModelBuilderCommand
to decorate
- class nltk.inference.api.ParallelProverBuilder[source]¶
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.
- class nltk.inference.api.ParallelProverBuilderCommand[source]¶
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)[source]¶
- Parameters:
prover (Prover) – The theorem tool to execute with the assumptions
- See:
BaseTheoremToolCommand
- 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.ProverCommand[source]¶
Bases:
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.ProverCommandDecorator[source]¶
Bases:
TheoremToolCommandDecorator
,ProverCommand
A base decorator for the
ProverCommand
class from which other prover command decorators can extend.- 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
- 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.
- class nltk.inference.api.TheoremToolCommandDecorator[source]¶
Bases:
TheoremToolCommand
A base decorator for the
ProverCommandDecorator
andModelBuilderCommandDecorator
classes from which decorators can extend.
- class nltk.inference.api.TheoremToolThread[source]¶
Bases:
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 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()[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.