Source Code for Module nltk.inference.mace

  1  # Natural Language Toolkit: Interface to the Mace4 Model Builder 
 
  2  #
 
  3  # Author: Dan Garrette <[email protected]>
 
  4  #         Ewan Klein <[email protected]>
 
  5  
 
  6  # URL: <http://nltk.org>
 
  7  # For license information, see LICENSE.TXT
 
  8  
 
  9  import os 
 10  import tempfile 
 11  from string import join 
 12  from nltk.sem.logic import * 
 13  from nltk.sem import Valuation 
 14  from api import ModelBuilder, ModelBuilderCommand 
 15  import prover9 
 16  from prover9 import Prover9Parent, Prover9CommandParent, \
 
 17                      call_mace4, call_interpformat 
 18  
 
 19  """
 
 20  A model builder that makes use of the external 'Mace4' package.
 
 21  """ 
 22  
 
 23 -class MaceCommand(Prover9CommandParent, ModelBuilderCommand): 
 24      """
 
 25      A L{MaceCommand} specific to the L{Mace} model builder.  It contains
 
 26      the a print_assumptions() method that is used to print the list
 
 27      of assumptions in multiple formats.
 
 28      """ 
 29 -    def __init__(self, goal=None, assumptions=[], timeout=60): 
 30          """
 
 31          @param goal: Input expression to prove
 
 32          @type goal: L{logic.Expression}
 
 33          @param assumptions: Input expressions to use as assumptions in
 
 34              the proof.
 
 35          @type assumptions: C{list} of L{logic.Expression}
 
 36          @param timeout: number of seconds before timeout; set to 0 for
 
 37              no timeout.
 
 38          @type timeout: C{int}
 
 39          """ 
 40          ModelBuilderCommand.__init__(self, Mace(timeout), goal, assumptions) 
 41          
 
 42 -    def convert2val(self): 
 43          """
 
 44          Transform the output file into an NLTK-style Valuation. 
 
 45          
 
 46          @return: A model if one is generated; None otherwise.
 
 47          @rtype: L{nltk.sem.Valuation} 
 
 48          """ 
 49          valuation = None 
 50          if self.build_model(): 
 51              valuation_standard_format = self._transform_output('standard') 
 52              
 
 53              d = {} 
 54              for line in valuation_standard_format.splitlines(False): 
 55                  l = line.strip() 
 56                  # find the number of entities in the model
 
 57                  if l.startswith('interpretation'): 
 58                      num_entities = int(l[l.index('(')+1:l.index(',')].strip()) 
 59                  # replace the integer identifier with a corresponding alphabetic character
 
 60                  elif l.startswith('function') and l.find('_') == -1: 
 61                      name = l[l.index('(')+1:l.index(',')].strip() 
 62                      if is_indvar(name): 
 63                          name = name.upper() 
 64                      d[name] = MaceCommand._make_model_var(int(l[l.index('[')+1:l.index(']')].strip())) 
 65                  
 
 66                  elif l.startswith('relation'): 
 67                      name = l[l.index('(')+1:l.index('(', l.index('(')+1)].strip() 
 68                      values = [int(v.strip()) for v in l[l.index('[')+1:l.index(']')].split(',')] 
 69                      d[name] = MaceCommand._make_model_dict(num_entities, values) 
 70                      
 
 71              valuation = Valuation(d.items()) 
 72          return valuation 
 73          
 
 74 -    def _make_model_dict(num_entities, values): 
 75          """
 
 76          Convert a Mace4-style relation table into a dictionary.
 
 77          
 
 78          @parameter num_entities: the number of entities in the model; determines the row length in the table.
 
 79          @type num_entities: C{int}
 
 80          @parameter values: integers that represent semantic values in a Mace4 model.
 
 81          @type values: C{list} of C{int}
 
 82          """ 
 83          if len(values) == 1: 
 84              return (values[0] == 1) 
 85          else: 
 86              d = {} 
 87              for i in range(num_entities): 
 88                  size = len(values) / num_entities 
 89                  d[MaceCommand._make_model_var(i)] = \
 
 90                      MaceCommand._make_model_dict(num_entities, values[i*size:(i+1)*size]) 
 91              return d 
 92          
 
 93      _make_model_dict = staticmethod(_make_model_dict) 
 94                  
 
 95 -    def _make_model_var(value): 
 96          """
 
 97          Pick an alphabetic character as identifier for an entity in the model.
 
 98          
 
 99          @parameter value: where to index into the list of characters
 
100          @type value: C{int}
 
101          """ 
102          letter = ['a','b','c','d','e','f','g','h','i','j','k','l','m','n',
 
103                    'o','p','q','r','s','t','u','v','w','x','y','z'][value] 
104          num = int(value) / 26 
105          if num > 0: 
106              return letter + str(num) 
107          else: 
108              return letter 
109          
 
110      _make_model_var = staticmethod(_make_model_var) 
111                  
 
112 -    def show_model(self, format=None): 
113          """
 
114          Print out a Mace4 model using any Mace4 C{interpformat} format. 
 
115          See U{http://www.cs.unm.edu/~mccune/mace4/manual/} for details.
 
116          
 
117          @parameter format: Output format for displaying
 
118          models. Defaults to 'standard' format.
 
119          @type format: C{str}
 
120          """ 
121          if not self._valuation: 
122              raise ValueError("You have to call build_model() first to "
 
123                               "get a model!") 
124          if not format: 
125              print self._valuation 
126          else: 
127              print self._transform_output(format) 
128  
 
129 -    def _transform_output(self, format): 
130          """
 
131          Transform the output file into any Mace4 C{interpformat} format. 
 
132          
 
133          @parameter format: Output format for displaying models. 
 
134          @type format: C{str}
 
135          """ 
136          if format in ['standard', 'standard2', 'portable', 'tabular', 
 
137                        'raw', 'cooked', 'xml', 'tex']: 
138              return call_interpformat(self._valuation, [format])[0] 
139          else: 
140              print "The specified format does not exist" 
141  
 
142 -class Mace(Prover9Parent, ModelBuilder): 
143      _valuation = None #: text output from running mace 
144  
 
145 -    def build_model(self, goal=None, assumptions=[], verbose=False): 
146          """
 
147          Use Mace4 to build a first order model.
 
148          
 
149          @return: C{True} if a model was found (i.e. Mace returns value of 0),
 
150          else C{False}        
 
151          """ 
152          stdout, returncode = call_mace4(self.prover9_input(goal, assumptions)) 
153          return (returncode == 0, stdout) 
154  
 
155 -def spacer(num=30): 
156      print '-' * num 
157      
 
158 -def decode_result(found): 
159      """
 
160      Decode the result of model_found() 
 
161      
 
162      @parameter found: The output of model_found() 
 
163      @type found: C{boolean}
 
164      """ 
165      return {True: 'Countermodel found', False: 'No countermodel found', None: 'None'}[found] 
166  
 
167 -def test_model_found(arguments): 
168      """
 
169      Try some proofs and exhibit the results.
 
170      """ 
171      for (goal, assumptions) in arguments: 
172          g = LogicParser().parse(goal) 
173          alist = [LogicParser().parse(a) for a in assumptions] 
174          m = MaceCommand(g, assumptions=alist, timeout=5) 
175          found = m.build_model() 
176          for a in alist: 
177              print '   %s' % a 
178          print '|- %s: %s\n' % (g, decode_result(found)) 
179          
 
180          
 
181 -def test_build_model(arguments): 
182      """
 
183      Try to build a L{nltk.sem.Valuation}.
 
184      """ 
185      g = LogicParser().parse('all x.man(x)') 
186      alist = [LogicParser().parse(a) for a in ['man(John)', 
 
187                                                'man(Socrates)', 
 
188                                                'man(Bill)', 
 
189                                                'some x.((not (x = John)) and (man(x) and sees(John,x)))',
 
190                                                'some x.((not (x = Bill)) and man(x))',
 
191                                                'all x.some y.(man(x) -> gives(Socrates,x,y))']] 
192      
 
193      m = MaceCommand(g, assumptions=alist) 
194      m.build_model() 
195      spacer() 
196      print "Assumptions and Goal" 
197      spacer() 
198      for a in alist: 
199          print '   %s' % a 
200      print '|- %s: %s\n' % (g, decode_result(m.build_model())) 
201      spacer() 
202      #m.show_model('standard')
 
203      #m.show_model('cooked')
 
204      print "Valuation" 
205      spacer() 
206      print m.convert2val(), '\n' 
207  
 
208 -def test_transform_output(argument_pair): 
209      """
 
210      Transform the model into various Mace4 C{interpformat} formats.
 
211      """ 
212      g = LogicParser().parse(argument_pair[0]) 
213      alist = [LogicParser().parse(a) for a in argument_pair[1]] 
214      m = MaceCommand(g, assumptions=alist) 
215      m.build_model() 
216      for a in alist: 
217          print '   %s' % a 
218      print '|- %s: %s\n' % (g, m.build_model()) 
219      for format in ['standard', 'portable', 'xml', 'cooked']: 
220          spacer() 
221          print "Using '%s' format" % format  
222          spacer() 
223          m.show_model(format=format) 
224          
 
225 -def test_make_model_dict(): 
226      print MaceCommand._make_model_dict(num_entities=3, values=[1,0,1]) 
227      print MaceCommand._make_model_dict(num_entities=3, values=[0,0,0,0,0,0,1,0,0]) 
228      
 
229  arguments = [
 
230      ('mortal(Socrates)', ['all x.(man(x) -> mortal(x))', 'man(Socrates)']),
 
231      ('(not mortal(Socrates))', ['all x.(man(x) -> mortal(x))', 'man(Socrates)'])
 
232  ] 
233  
 
234  if __name__ == '__main__': 
235      test_model_found(arguments) 
236      test_build_model(arguments) 
237      test_transform_output(arguments[1]) 
238      
 
239      a = LogicParser().parse('(see(mary,john) & -(mary = john))') 
240      mb = MaceCommand(assumptions=[a]) 
241      mb.build_model() 
242      print mb.convert2val() 
243