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 counter-model, 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, the ModelBuilder 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, the Prover 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: builtins.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, the ModelBuilder 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: builtins.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, the Prover 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: builtins.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 and ModelBuilderCommandDecorator 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 si. 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 si -rj. For example:
s0 readings:
s0-r1: some x.(boxer(x) & walk(x))
s0-r0: some x.(boxerdog(x) & walk(x))
A “thread” is a list of readings, represented as a list of rids. Each thread receives a “thread ID” (tid) of the form di. For example:
d0: ['s0-r0', 's1-r0']
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: builtins.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 and self._sentences. :param sentence: An input sentence :type sentence: str :param informchk: if True, check that the result of adding the sentence is thread-informative. Updates self._readings. :param consistchk: if True, check that the result of adding the sentence is thread-consistent. Updates self._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: - thread_id (str) – thread ID
- threads (dict) – a mapping from thread IDs to lists of reading IDs
Returns: A list of pairs (rid, reading) where reading is the logic.Expression associated with a reading ID
Return 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 in readings.
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: builtins.object
- combine_readings(readings)[source]¶
Parameters: readings (list(Expression)) – readings to combine Returns: one combined reading 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.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 the Mace model builder. It contains a print_assumptions() method that is used to print the list of assumptions in multiple formats.
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: builtins.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.SetHolder[source]¶
Bases: builtins.list
A list of sets of Variables.
- 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 the Prover9 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: builtins.object
A common base class used by both Prover9Command and MaceCommand, which is responsible for maintaining a goal and a set of assumptions, and generating prover9-style input files from them.
- exception nltk.inference.prover9.Prover9Exception(returncode, message)[source]¶
Bases: builtins.Exception
- class nltk.inference.prover9.Prover9Parent[source]¶
Bases: builtins.object
A common class extended by both Prover9 and Mace <mace.Mace>. It contains the functionality required to convert NLTK-style expressions into Prover9-style expressions.
nltk.inference.resolution module¶
Module for a resolution-based First Order theorem prover.
- class nltk.inference.resolution.BindingDict(binding_list=None)[source]¶
Bases: builtins.object
- unicode_repr()¶
- class nltk.inference.resolution.Clause(data)[source]¶
Bases: builtins.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
- 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 resulting Clause objects that could be obtained by unification
- 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
nltk.inference.tableau module¶
Module for a tableau-based First Order theorem prover.
- class nltk.inference.tableau.Categories[source]¶
Bases: builtins.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.