Package nltk :: Package inference :: Module nonmonotonic :: Class ClosedDomainProver

type ClosedDomainProver

                 object --+            
                          |            
     api.TheoremToolCommand --+        
                              |        
api.TheoremToolCommandDecorator --+    
                                  |    
                 object --+       |    
                          |       |    
     api.TheoremToolCommand --+   |    
                              |   |    
              api.ProverCommand --+    
                                  |    
         api.ProverCommandDecorator --+
                                      |
                                     ClosedDomainProver

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

Instance Methods

[hide private]

assumptions(self)
List the current assumptions.

source code

goal(self)
Return the goal

source code

replace_quants(self, ex, domain)
Apply the closed domain assumption to the expression

source code

Inherited from api.ProverCommandDecorator: __init__, decorate_proof, get_prover, proof, prove

Inherited from api.TheoremToolCommandDecorator: add_assumptions, print_assumptions, retract_assumptions

Method Details

[hide private]

assumptions(self)

source code

List the current assumptions.

Returns:: list of Expression
Overrides: api.TheoremToolCommand.assumptions: (inherited documentation)

goal(self)

source code

Return the goal

Returns:: Expression
Overrides: api.TheoremToolCommand.goal: (inherited documentation)

replace_quants(self, ex, domain)

source code

Apply the closed domain assumption to the expression

Domain = union([e.free(False) 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