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.

assumptions()[source]

List the current assumptions.

Returns:

list of Expression

goal()[source]

Return the goal

Returns:

Expression

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:
  • exExpression

  • 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)

assumptions()[source]

List the current assumptions.

Returns:

list of Expression

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

__init__()[source]
append_prop(new_prop)[source]
append_sig(new_sig)[source]
validate_sig_len(new_sig)[source]
exception nltk.inference.nonmonotonic.ProverParseError[source]

Bases: Exception

class nltk.inference.nonmonotonic.SetHolder[source]

Bases: list

A list of sets of Variables.

class nltk.inference.nonmonotonic.UniqueNamesProver[source]

Bases: ProverCommandDecorator

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

assumptions()[source]
  • 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()[source]
nltk.inference.nonmonotonic.closed_world_demo()[source]
nltk.inference.nonmonotonic.combination_prover_demo()[source]
nltk.inference.nonmonotonic.default_reasoning_demo()[source]
nltk.inference.nonmonotonic.demo()[source]
nltk.inference.nonmonotonic.get_domain(goal, assumptions)[source]
nltk.inference.nonmonotonic.print_proof(goal, premises)[source]
nltk.inference.nonmonotonic.unique_names_demo()[source]