nltk.inference package¶
Submodules¶
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 countermodel, in the sense of a model that will satisfy
the assumptions plus the negation of G.

class
nltk.inference.api.
BaseModelBuilderCommand
(modelbuilder, goal=None, assumptions=None)[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.

class
nltk.inference.api.
BaseProverCommand
(prover, goal=None, assumptions=None)[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.
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
(goal=None, assumptions=None)[source]¶ Bases:
nltk.inference.api.TheoremToolCommand
This class holds a goal and a list of assumptions to be used in proving or model building.

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

class
nltk.inference.api.
ModelBuilderCommandDecorator
(modelBuilderCommand)[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.

class
nltk.inference.api.
ParallelProverBuilder
(prover, modelbuilder)[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
(prover, modelbuilder, goal=None, assumptions=None)[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”.

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:
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.
ProverCommandDecorator
(proverCommand)[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.
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
(command)[source]¶ Bases:
nltk.inference.api.TheoremToolCommand
A base decorator for the
ProverCommandDecorator
andModelBuilderCommandDecorator
classes from which decorators can extend.
nltk.inference.discourse module¶
Module for incrementally developing simple discourses, and checking for semantic ambiguity, consistency and informativeness.
Many of the ideas are based on the CURT family of programs of Blackburn and Bos (see http://homepages.inf.ed.ac.uk/jbos/comsem/book1.html).
Consistency checking is carried out by using the mace
module to call the Mace4 model builder.
Informativeness checking is carried out with a call to Prover.prove()
from
the inference
module.
DiscourseTester
is a constructor for discourses.
The basic data structure is a list of sentences, stored as self._sentences
. Each sentence in the list
is assigned a “sentence ID” (sid
) of the form s
i. For example:
s0: A boxer walks
s1: Every boxer chases a girl
Each sentence can be ambiguous between a number of readings, each of which receives a
“reading ID” (rid
) of the form s
i r
j. For example:
s0 readings:
s0r1: some x.(boxer(x) & walk(x))
s0r0: some x.(boxerdog(x) & walk(x))
A “thread” is a list of readings, represented as a list of rid
s.
Each thread receives a “thread ID” (tid
) of the form d
i.
For example:
d0: ['s0r0', 's1r0']
The set of all threads for a discourse is the Cartesian product of all the readings of the sequences of sentences.
(This is not intended to scale beyond very short discourses!) The method readings(filter=True)
will only show
those threads which are consistent (taking into account any background assumptions).

class
nltk.inference.discourse.
DiscourseTester
(input, reading_command=None, background=None)[source]¶ Bases:
object
Check properties of an ongoing discourse.

add_background
(background, verbose=False)[source]¶ Add a list of background assumptions for reasoning about the discourse.
When called, this method also updates the discourse model’s set of readings and threads. :param background: Formulas which contain background information :type background: list(Expression)

add_sentence
(sentence, informchk=False, consistchk=False)[source]¶ Add a sentence to the current discourse.
Updates
self._input
andself._sentences
. :param sentence: An input sentence :type sentence: str :param informchk: ifTrue
, check that the result of adding the sentence is threadinformative. Updatesself._readings
. :param consistchk: ifTrue
, check that the result of adding the sentence is threadconsistent. Updatesself._readings
.

expand_threads
(thread_id, threads=None)[source]¶ Given a thread ID, find the list of
logic.Expression
objects corresponding to the reading IDs in that thread.Parameters: Returns: A list of pairs
(rid, reading)
where reading is thelogic.Expression
associated with a reading IDReturn type: list of tuple

models
(thread_id=None, show=True, verbose=False)[source]¶ Call Mace4 to build a model for each current discourse thread.
Parameters:  thread_id (str) – thread ID
 show – If
True
, display the model that has been found.

static
multiply
(discourse, readings)[source]¶ Multiply every thread in
discourse
by every reading inreadings
.Given discourse = [[‘A’], [‘B’]], readings = [‘a’, ‘b’, ‘c’] , returns [[‘A’, ‘a’], [‘A’, ‘b’], [‘A’, ‘c’], [‘B’, ‘a’], [‘B’, ‘b’], [‘B’, ‘c’]]
Parameters:  discourse (list of lists) – the current list of readings
 readings (list(Expression)) – an additional list of readings
Return type: A list of lists

readings
(sentence=None, threaded=False, verbose=True, filter=False, show_thread_readings=False)[source]¶ Construct and show the readings of the discourse (or of a single sentence).
Parameters:  sentence (str) – test just this sentence
 threaded – if
True
, print out each thread ID and the corresponding thread.  filter – if
True
, only print out consistent thread IDs and threads.


class
nltk.inference.discourse.
DrtGlueReadingCommand
(semtype_file=None, remove_duplicates=False, depparser=None)[source]¶

class
nltk.inference.discourse.
ReadingCommand
[source]¶ Bases:
object

combine_readings
(readings)[source]¶ Parameters: readings (list(Expression)) – readings to combine Returns: one combined reading Return type: Expression

process_thread
(sentence_readings)[source]¶ This method should be used to handle dependencies between readings such as resolving anaphora.
Parameters: sentence_readings (list(Expression)) – readings to process Returns: the list of readings after processing Return type: list(Expression)

to_fol
(expression)[source]¶ Convert this expression into a FirstOrder Logic expression.
Parameters: expression (Expression) – an expression Returns: a FOL version of the input expression Return type: Expression


nltk.inference.discourse.
discourse_demo
(reading_command=None)[source]¶ Illustrate the various methods of
DiscourseTester

nltk.inference.discourse.
drt_discourse_demo
(reading_command=None)[source]¶ Illustrate the various methods of
DiscourseTester

nltk.inference.discourse.
load_fol
(s)[source]¶ Temporarily duplicated from
nltk.sem.util
. Convert a file of first order formulas into a list ofExpression
objects.Parameters: s (str) – the contents of the file Returns: a list of parsed formulas. Return type: list(Expression)
nltk.inference.mace module¶
A model builder that makes use of the external ‘Mace4’ package.

class
nltk.inference.mace.
Mace
(end_size=500)[source]¶ Bases:
nltk.inference.prover9.Prover9Parent
,nltk.inference.api.ModelBuilder

class
nltk.inference.mace.
MaceCommand
(goal=None, assumptions=None, max_models=500, model_builder=None)[source]¶ Bases:
nltk.inference.prover9.Prover9CommandParent
,nltk.inference.api.BaseModelBuilderCommand
A
MaceCommand
specific to theMace
model builder. It contains a print_assumptions() method that is used to print the list of assumptions in multiple formats.
valuation
¶

nltk.inference.nonmonotonic module¶
A module to perform nonmonotonic reasoning. The ideas and demonstrations in this module are based on “Logical Foundations of Artificial Intelligence” by Michael R. Genesereth and Nils J. Nilsson.

class
nltk.inference.nonmonotonic.
ClosedDomainProver
(proverCommand)[source]¶ Bases:
nltk.inference.api.ProverCommandDecorator
This is a prover decorator that adds domain closure assumptions before proving.

replace_quants
(ex, domain)[source]¶  Apply the closed domain assumption to the expression
 Domain = union([e.free()e.constants() for e in all_expressions])
 translate “exists x.P” to “(z=d1  z=d2  ... ) & P.replace(x,z)” OR
 “P.replace(x, d1)  P.replace(x, d2)  ...”
 translate “all x.P” to “P.replace(x, d1) & P.replace(x, d2) & ...”
Parameters:  ex –
Expression
 domain – set of {Variable}s
Returns: Expression


class
nltk.inference.nonmonotonic.
ClosedWorldProver
(proverCommand)[source]¶ Bases:
nltk.inference.api.ProverCommandDecorator
This is a prover decorator that completes predicates before proving.
If the assumptions contain “P(A)”, then “all x.(P(x) > (x=A))” is the completion of “P”. If the assumptions contain “all x.(ostrich(x) > bird(x))”, then “all x.(bird(x) > ostrich(x))” is the completion of “bird”. If the assumptions don’t contain anything that are “P”, then “all x.P(x)” is the completion of “P”.
walk(Socrates) Socrates != Bill + all x.(walk(x) > (x=Socrates)) ————— walk(Bill)
see(Socrates, John) see(John, Mary) Socrates != John John != Mary + all x.all y.(see(x,y) > ((x=Socrates & y=John)  (x=John & y=Mary))) ————— see(Socrates, Mary)
all x.(ostrich(x) > bird(x)) bird(Tweety) ostrich(Sam) Sam != Tweety + all x.(bird(x) > (ostrich(x)  x=Tweety)) + all x.ostrich(x) —————— bird(Sam)

class
nltk.inference.nonmonotonic.
PredHolder
[source]¶ Bases:
object
This class will be used by a dictionary that will store information about predicates to be used by the
ClosedWorldProver
.The ‘signatures’ property is a list of tuples defining signatures for which the predicate is true. For instance, ‘see(john, mary)’ would be result in the signature ‘(john,mary)’ for ‘see’.
The second element of the pair is a list of pairs such that the first element of the pair is a tuple of variables and the second element is an expression of those variables that makes the predicate true. For instance, ‘all x.all y.(see(x,y) > know(x,y))’ would result in “((x,y),(‘see(x,y)’))” for ‘know’.

unicode_repr
()¶


class
nltk.inference.nonmonotonic.
UniqueNamesProver
(proverCommand)[source]¶ Bases:
nltk.inference.api.ProverCommandDecorator
This is a prover decorator that adds unique names assumptions before proving.
nltk.inference.prover9 module¶
A theorem prover that makes use of the external ‘Prover9’ package.

class
nltk.inference.prover9.
Prover9
(timeout=60)[source]¶ Bases:
nltk.inference.prover9.Prover9Parent
,nltk.inference.api.Prover

class
nltk.inference.prover9.
Prover9Command
(goal=None, assumptions=None, timeout=60, prover=None)[source]¶ Bases:
nltk.inference.prover9.Prover9CommandParent
,nltk.inference.api.BaseProverCommand
A
ProverCommand
specific to theProver9
prover. It contains the a print_assumptions() method that is used to print the list of assumptions in multiple formats.

class
nltk.inference.prover9.
Prover9CommandParent
[source]¶ Bases:
object
A common base class used by both
Prover9Command
andMaceCommand
, which is responsible for maintaining a goal and a set of assumptions, and generating prover9style input files from them.

class
nltk.inference.prover9.
Prover9Parent
[source]¶ Bases:
object
A common class extended by both
Prover9
andMace <mace.Mace>
. It contains the functionality required to convert NLTKstyle expressions into Prover9style expressions.
nltk.inference.resolution module¶
Module for a resolutionbased First Order theorem prover.

class
nltk.inference.resolution.
BindingDict
(binding_list=None)[source]¶ Bases:
object

unicode_repr
()¶


class
nltk.inference.resolution.
Clause
(data)[source]¶ Bases:
list

isSubsetOf
(other)[source]¶ Return True iff every term in ‘self’ is a term in ‘other’.
Parameters: other – Clause
Returns: bool

is_tautology
()[source]¶ Self is a tautology if it contains ground terms P and P. The ground term, P, must be an exact match, ie, not using unification.

replace
(variable, expression)[source]¶ Replace every instance of variable with expression across every atom in the clause
Parameters:  variable –
Variable
 expression –
Expression
 variable –

substitute_bindings
(bindings)[source]¶ Replace every binding
Parameters: bindings – A list of tuples mapping Variable Expressions to the Expressions to which they are bound :return:
Clause

subsumes
(other)[source]¶ Return True iff ‘self’ subsumes ‘other’, this is, if there is a substitution such that every term in ‘self’ can be unified with a term in ‘other’.
Parameters: other – Clause
Returns: bool

unicode_repr
()¶

unify
(other, bindings=None, used=None, skipped=None, debug=False)[source]¶ Attempt to unify this Clause with the other, returning a list of resulting, unified, Clauses.
Parameters:  other –
Clause
with which to unify  bindings –
BindingDict
containing bindings that should be used
during the unification :param used: tuple of two lists of atoms. The first lists the atoms from ‘self’ that were successfully unified with atoms from ‘other’. The second lists the atoms from ‘other’ that were successfully unified with atoms from ‘self’. :param skipped: tuple of two
Clause
objects. The first is a list of all the atoms from the ‘self’ Clause that have not been unified with anything on the path. The second is same thing for the ‘other’ Clause. :param debug: bool indicating whether debug statements should print :return: list containing all the resultingClause
objects that could be obtained by unification other –


class
nltk.inference.resolution.
ResolutionProver
[source]¶ Bases:
nltk.inference.api.Prover

ANSWER_KEY
= 'ANSWER'¶


class
nltk.inference.resolution.
ResolutionProverCommand
(goal=None, assumptions=None, prover=None)[source]¶

nltk.inference.resolution.
clausify
(expression)[source]¶ Skolemize, clausify, and standardize the variables apart.

nltk.inference.resolution.
most_general_unification
(a, b, bindings=None)[source]¶ Find the most general unification of the two given expressions
Parameters:  a –
Expression
 b –
Expression
 bindings –
BindingDict
a starting set of bindings with which the unification must be consistent
Returns: a list of bindings
Raises: BindingException – if the Expressions cannot be unified
 a –
nltk.inference.tableau module¶
Module for a tableaubased First Order theorem prover.

class
nltk.inference.tableau.
Categories
[source]¶ Bases:
object

ALL
= 20¶

AND
= 10¶

APP
= 4¶

ATOM
= 0¶

D_NEG
= 7¶

EQ
= 18¶

EXISTS
= 19¶

IFF
= 16¶

IMP
= 14¶

N_ALL
= 8¶

N_AND
= 15¶

N_APP
= 5¶

N_ATOM
= 2¶

N_EQ
= 6¶

N_EXISTS
= 9¶

N_IFF
= 17¶

N_IMP
= 12¶

N_OR
= 11¶

N_PROP
= 3¶

OR
= 13¶

PROP
= 1¶


class
nltk.inference.tableau.
TableauProver
[source]¶ Bases:
nltk.inference.api.Prover
Module contents¶
Classes and interfaces for theorem proving and model building.