Package nltk :: Package inference :: Module nonmonotonic :: Class UniqueNamesProver

type UniqueNamesProver

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

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

Instance Methods

[hide private]

assumptions(self)
Domain = union([e.free(False) for e in all_expressions])

source code

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

Inherited from api.TheoremToolCommandDecorator: add_assumptions, goal, print_assumptions, retract_assumptions

Method Details

[hide private]

assumptions(self)

source code

Domain = union([e.free(False) for e in all_expressions])
if "d1 = d2" cannot be proven from the premises, then add "d1 != d2"

Returns:: list of Expression
Overrides: api.TheoremToolCommand.assumptions