Source Code for Module nltk.inference.inference

 1  # Natural Language Toolkit: Interface to Theorem Provers 
 
 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  from nltk.sem import logic  
10  
 
11  import api 
12  import tableau 
13  import prover9 
14  import mace 
15  
 
16  """
 
17  A wrapper module that calls theorem provers and model builders.
 
18  """ 
19  
 
20 -def get_prover(goal=None, assumptions=[], prover_name='Prover9'): 
21      """
 
22      @param goal: Input expression to prove
 
23      @type goal: L{logic.Expression}
 
24      @param assumptions: Input expressions to use as assumptions in the proof
 
25      @type assumptions: L{list} of logic.Expression objects
 
26      """ 
27      if prover_name.lower() == 'tableau': 
28          return api.ProverCommand(tableau.Tableau(), goal, assumptions) 
29      elif prover_name.lower() == 'prover9': 
30          return prover9.Prover9Command(goal, assumptions) 
31  
 
32 -def get_model_builder(goal=None, assumptions=[], model_builder_name='Mace'): 
33      """
 
34      @param goal: Input expression to prove
 
35      @type goal: L{logic.Expression}
 
36      @param assumptions: Input expressions to use as assumptions in the proof
 
37      @type assumptions: L{list} of logic.Expression objects
 
38      """ 
39      if model_builder_name.lower() == 'mace': 
40          return mace.MaceCommand(goal, assumptions) 
41  
 
42 -def demo(): 
43      lp = logic.LogicParser() 
44      a = lp.parse(r'some x.(man(x) and walks(x))') 
45      b = lp.parse(r'some x.(walks(x) and man(x))') 
46      bicond = logic.IffExpression(a, b) 
47      print "Trying to prove:\n '%s <-> %s'" % (a, b) 
48      print 'tableau: %s' % get_prover(bicond, prover_name='tableau').prove() 
49      print 'Prover9: %s' % get_prover(bicond, prover_name='Prover9').prove() 
50      print '\n' 
51      
 
52      lp = logic.LogicParser() 
53      a = lp.parse(r'all x.(man(x) -> mortal(x))') 
54      b = lp.parse(r'man(socrates)') 
55      c1 = lp.parse(r'mortal(socrates)') 
56      c2 = lp.parse(r'-mortal(socrates)') 
57  
 
58      print get_prover(c1, [a,b], 'prover9').prove() 
59      print get_prover(c2, [a,b], 'prover9').prove() 
60      print get_model_builder(c1, [a,b], 'mace').build_model() 
61      print get_model_builder(c2, [a,b], 'mace').build_model() 
62  
 
63  if __name__ == '__main__':  
64      demo() 
65