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[source]¶
Bases:
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[source]¶
Bases:
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’.
- class nltk.inference.nonmonotonic.UniqueNamesProver[source]¶
Bases:
ProverCommandDecorator
This is a prover decorator that adds unique names assumptions before proving.