Package nltk :: Package inference :: Module nonmonotonic :: Class ClosedWorldProver

Class ClosedWorldProver

            object --+    
                     |    
ProverCommandDecorator --+
                         |
                        ClosedWorldProver

This is a prover decorator that completes predicates before proving.

If the premises don't logically entail "P(A)" then add "-P(A)" all x.(P(x) -> (x=A)) 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)) ------------------- -bird(Sam)

Instance Methods

[hide private]

assumptions(self)

source code

_make_unique_signature(self, predHolder)
This method figures out how many arguments the predicate takes and returns a tuple containing that number of unique variables.

source code

_make_antecedent(self, predicate, signature)

source code

_make_predicate_dict(self, assumptions)
Create a dictionary of predicates from the assumptions.

source code

_map_predicates(self, expression, predDict)

source code

goal(self)

source code

Inherited from ProverCommandDecorator: __init__, add_assumptions, get_prover, print_assumptions, prove, retract_assumptions

Inherited from object: __delattr__, __getattribute__, __hash__, __new__, __reduce__, __reduce_ex__, __repr__, __setattr__, __str__

Properties

[hide private]

Inherited from object: __class__

Method Details

[hide private]

_make_predicate_dict(self, assumptions)

source code

Create a dictionary of predicates from the assumptions.

Parameters:

assumptions - a list of Expressions

Returns:

dict mapping VariableExpressions to of PredHolders