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

Bases: ProverCommandDecorator

This is a prover decorator that adds domain closure assumptions before proving.

assumptions()

List the current assumptions.

Returns

list of Expression

goal()

Return the goal

Returns

Expression

replace_quants(ex, domain)

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

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)

assumptions()

List the current assumptions.

Returns

list of Expression

class nltk.inference.nonmonotonic.PredHolder

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

__init__()

append_prop(new_prop)

append_sig(new_sig)

validate_sig_len(new_sig)

exception nltk.inference.nonmonotonic.ProverParseError

Bases: Exception

class nltk.inference.nonmonotonic.SetHolder

Bases: list

A list of sets of Variables.

class nltk.inference.nonmonotonic.UniqueNamesProver

Bases: ProverCommandDecorator

This is a prover decorator that adds unique names assumptions before proving.

assumptions()

• Domain = union([e.free()|e.constants() for e in all_expressions])

• if “d1 = d2” cannot be proven from the premises, then add “d1 != d2”

nltk.inference.nonmonotonic.closed_domain_demo()

nltk.inference.nonmonotonic.closed_world_demo()

nltk.inference.nonmonotonic.combination_prover_demo()

nltk.inference.nonmonotonic.default_reasoning_demo()

nltk.inference.nonmonotonic.demo()

nltk.inference.nonmonotonic.get_domain(goal, assumptions)

nltk.inference.nonmonotonic.print_proof(goal, premises)

nltk.inference.nonmonotonic.unique_names_demo()