Source Code for Module nltk.inference.api

  1  # Natural Language Toolkit: Classifier Interface 
  2  # 
  3  # Author: Ewan Klein <[email protected]> 
  4  #         Dan Garrette <[email protected]> 
  5  # 
  6  # URL: <http://nltk.org> 
  7  # For license information, see LICENSE.TXT 
  8   
  9  """ 
 10  Interfaces for theorem provers and model builders. 
 11   
 12  L{Prover} is a standard interface for a theorem prover which tries to prove a goal from a  
 13  list of assumptions. 
 14   
 15  L{ModelBuilder} is a standard interface for a model builder. Given just a set of assumptions. 
 16  the model builder tries to build a model for the assumptions. Given a set of assumptions and a  
 17  goal M{G}, the model builder tries to find a counter-model, in the sense of a model that will satisfy 
 18  the assumptions plus the negation of M{G}.  
 19  """ 
 20   
 21 -class Prover(object): 
 22      """ 
 23      Interface for trying to prove a goal from assumptions.  
 24      Both the goal and the assumptions are  
 25      constrained to be formulas of L{logic.Expression}. 
 26      """ 
 27 -    def prove(self, goal=None, assumptions=[], verbose=False): 
 28          """ 
 29          @return: Whether the proof was successful or not. 
 30          @rtype: C{bool}  
 31          """ 
 32          raise NotImplementedError() 
 33       
 34 -class ModelBuilder(object): 
 35      """ 
 36      Interface for trying to build a model of set of formulas. 
 37      Open formulas are assumed to be universally quantified. 
 38      Both the goal and the assumptions are  
 39      constrained to be formulas of L{logic.Expression}. 
 40      """ 
 41 -    def build_model(self, goal=None, assumptions=[], verbose=False): 
 42          """ 
 43          @return: A model if one is generated; None otherwise. 
 44          @rtype: C{nltk.sem.evaluate.Valuation}  
 45          """ 
 46          raise NotImplementedError() 
 47   
 48   
 49 -class TheoremToolCommand(object): 
 50      """ 
 51      This class holds a goal and a list of assumptions to be used in proving 
 52      or model building. 
 53      """ 
 54 -    def __init__(self, goal=None, assumptions=[]): 
 55          """ 
 56          @param goal: Input expression to prove 
 57          @type goal: L{logic.Expression} 
 58          @param assumptions: Input expressions to use as assumptions in  
 59              the proof. 
 60          @type assumptions: C{list} of L{logic.Expression} 
 61          """ 
 62          self._goal = goal 
 63          """The logic expression to prove. 
 64             L{logic.Expression}""" 
 65           
 66          self._assumptions = list(assumptions) 
 67          """The set of expressions to use as assumptions in the proof. 
 68             C{list} of L{logic.Expression}""" 
 69              
 70          self._result = None 
 71          """A holder for the result, so prevent unnecessary re-proving""" 
 72           
 73 -    def add_assumptions(self, new_assumptions): 
 74          """ 
 75          Add new assumptions to the assumption list. 
 76           
 77          @param new_assumptions: new assumptions 
 78          @type new_assumptions: C{list} of L{sem.logic.Expression}s 
 79          """ 
 80          self._assumptions += new_assumptions 
 81          self._result = None 
 82       
 83 -    def retract_assumptions(self, retracted, debug=False): 
 84          """ 
 85          Retract assumptions from the assumption list. 
 86           
 87          @param debug: If True, give warning when C{retracted} is not present on  
 88          assumptions list. 
 89          @type debug: C{bool} 
 90          @param retracted: assumptions to be retracted 
 91          @type retracted: C{list} of L{sem.logic.Expression}s 
 92          """ 
 93          retracted = set(retracted) 
 94          result_list = [a for a in self._assumptions if a not in retracted] 
 95          if debug and result_list == self._assumptions: 
 96              print Warning("Assumptions list has not been changed:") 
 97              self.assumptions() 
 98               
 99          self._assumptions = result_list 
100           
101          self._result = None 
102       
103 -    def assumptions(self): 
104          """ 
105          List the current assumptions.        
106          """ 
107          return self._assumptions 
108       
109 -    def goal(self): 
110          """ 
111          Return the goal 
112          """ 
113          return self._goal 
114           
115 -    def print_assumptions(self): 
116          """ 
117          Print the list of the current assumptions.        
118          """ 
119          for a in self.assumptions(): 
120              print a 
121   
122 -class ProverCommand(TheoremToolCommand): 
123      """ 
124      This class holds a C{Prover}, a goal, and a list of assumptions.  When 
125      prove() is called, the C{Prover} is executed with the goal and assumptions. 
126      """ 
127 -    def __init__(self, prover, goal=None, assumptions=[]): 
128          """ 
129          @param prover: The theorem tool to execute with the assumptions 
130          @type prover: C{Prover} 
131          @see: C{TheoremToolCommand} 
132          """ 
133          self._prover = prover 
134          """The theorem tool to execute with the assumptions""" 
135           
136          TheoremToolCommand.__init__(self, goal, assumptions) 
137           
138          self._proof = None 
139   
140 -    def prove(self, verbose=False): 
141          """ 
142          Perform the actual proof.  Store the result to prevent unnecessary 
143          re-proving. 
144          """ 
145          if self._result is None: 
146              self._result, self._proof = self._prover.prove(self.goal(),  
147                                                             self.assumptions(), 
148                                                             verbose) 
149          return self._result 
150   
151 -    def show_proof(self): 
152          print self._proof 
153   
154 -    def get_prover(self): 
155          return self._prover 
156       
157 -class ModelBuilderCommand(TheoremToolCommand): 
158      """ 
159      This class holds a C{ModelBuilder}, a goal, and a list of assumptions.  When 
160      build_model() is called, the C{ModelBuilder} is executed with the goal and  
161      assumptions. 
162      """ 
163 -    def __init__(self, modelbuilder, goal=None, assumptions=[]): 
164          """ 
165          @param modelbuilder: The theorem tool to execute with the assumptions 
166          @type modelbuilder: C{ModelBuilder} 
167          @see: C{TheoremToolCommand} 
168          """ 
169          self._modelbuilder = modelbuilder 
170          """The theorem tool to execute with the assumptions""" 
171           
172          TheoremToolCommand.__init__(self, goal, assumptions) 
173           
174          self._valuation = None 
175   
176 -    def build_model(self, verbose=False): 
177          """ 
178          Perform the actual proof.  Store the result to prevent unnecessary 
179          re-building. 
180          """ 
181          if self._result is None: 
182              self._result, self._valuation = \ 
183                      self._modelbuilder.build_model(self.goal(),  
184                                                     self.assumptions(), 
185                                                     verbose) 
186          return self._result 
187