Package nltk :: Package inference :: Module nonmonotonic
[hide private]
[frames] | no frames]

Source Code for Module nltk.inference.nonmonotonic

  1  # Natural Language Toolkit: Nonmonotonic Reasoning 
  2  # 
  3  # Author: Daniel H. Garrette <[email protected]> 
  4  # 
  5  # Copyright (C) 2001-2008 NLTK Project 
  6  # URL: <http://www.nltk.org> 
  7  # For license information, see LICENSE.TXT 
  8   
  9  """ 
 10  A module to perform nonmonotonic reasoning 
 11  """ 
 12   
 13  from nltk.sem.logic import * 
 14  from nltk.inference import inference 
 15  from nltk.inference.api import Prover 
 16  from nltk import defaultdict 
 17   
18 -class ProverCommandDecorator(object):
19 """ 20 A base decorator for the C{ProverCommand} class from which concrete 21 prover command decorators can extend. 22 """
23 - def __init__(self, proverCommand):
24 """ 25 @param proverCommand: C{ProverCommand} to decorate 26 """ 27 self._proverCommand = proverCommand
28
29 - def prove(self, verbose=False):
30 return self.get_prover().prove(self.goal(), 31 self.assumptions(), 32 verbose)[0]
33
34 - def get_prover(self):
35 return self._proverCommand.get_prover()
36
37 - def add_assumptions(self, new_assumptions):
38 self._proverCommand.add_assumptions(new_assumptions)
39
40 - def retract_assumptions(self, retracted, debug=False):
41 return self._proverCommand.retract_assumptions(retracted, debug)
42
43 - def print_assumptions(self):
44 self._proverCommand.print_assumptions()
45 46
47 -class ClosedDomainProver(ProverCommandDecorator):
48 """ 49 This is a prover decorator that adds domain closure assumptions before 50 proving. 51 """
52 - def assumptions(self):
53 """ 54 - Domain = union([e.free(False) for e in all_expressions]) 55 - translate "exists x.P" to "(z=d1 | z=d2 | ... ) & P.replace(x,z)" OR 56 "P.replace(x, d1) | P.replace(x, d2) | ..." 57 - translate "all x.P" to "P.replace(x, d1) & P.replace(x, d2) & ..." 58 """ 59 assumptions = [a for a in self._proverCommand.assumptions()] 60 61 domain = set() 62 for a in assumptions + [-self._proverCommand.goal()]: 63 domain |= (a.free(False) - a.free(True)) 64 65 new_assumptions = set() 66 self._handle_quant_ex(self._proverCommand.goal(), domain, assumptions) 67 while assumptions: 68 a = assumptions.pop() 69 if isinstance(a, VariableBinderExpression): 70 self._handle_quant_ex(a, domain, assumptions) 71 else: 72 new_assumptions.add(a) 73 74 return list(new_assumptions)
75
76 - def goal(self):
77 return self._proverCommand.goal()
78
79 - def _handle_quant_ex(self, ex, domain, assumptions):
80 if isinstance(ex, ExistsExpression): 81 newterms = [ex.term.replace(ex.variable, VariableExpression(d)) 82 for d in domain] 83 assumptions.append(reduce(Expression.__or__, newterms)) 84 elif isinstance(ex, AllExpression): 85 for d in domain: 86 assumptions.append(ex.term.replace(ex.variable, 87 VariableExpression(d)))
88
89 -class UniqueNamesProver(ProverCommandDecorator):
90 """ 91 This is a prover decorator that adds unique names assumptions before 92 proving. 93 """
94 - def assumptions(self):
95 """ 96 - Domain = union([e.free(False) for e in all_expressions]) 97 - if "d1 = d2" cannot be proven from the premises, then add "d1 != d2" 98 """ 99 assumptions = self._proverCommand.assumptions() 100 101 domain = set() 102 for a in assumptions: 103 domain |= (a.free(False) - a.free(True)) 104 domain = sorted(list(domain)) 105 106 #build a dictionary of obvious equalities 107 eq_dict = defaultdict(list) 108 for a in assumptions: 109 if isinstance(a, EqualityExpression): 110 av = a.first.variable 111 bv = a.second.variable 112 if av < bv: 113 eq_dict[av].append(bv) 114 else: 115 eq_dict[bv].append(av) 116 117 assumptions2 = [] 118 for i,a in enumerate(domain): 119 for b in domain[i+1:]: 120 if b not in eq_dict[a]: 121 newEqEx = EqualityExpression(VariableExpression(a), 122 VariableExpression(b)) 123 if not inference.get_prover(newEqEx, assumptions).prove(): 124 #if we can't prove it, then assume it's false 125 assumptions2.append(-newEqEx) 126 127 return assumptions + assumptions2
128
129 - def goal(self):
130 return self._proverCommand.goal()
131
132 -class ClosedWorldProver(ProverCommandDecorator):
133 """ 134 This is a prover decorator that completes predicates before proving. 135 136 If the premises don't logically entail "P(A)" then add "-P(A)" 137 all x.(P(x) -> (x=A)) is the completion of P 138 139 walk(Socrates) 140 Socrates != Bill 141 + all x.(walk(x) -> (x = Socrates)) 142 ---------------- 143 -walk(Bill) 144 145 see(Socrates, John) 146 see(John, Mary) 147 Socrates != John 148 John != Mary 149 + all x.all y.(see(x,y) -> ((x=Socrates & y=John) | (x=John & y=Mary))) 150 ---------------- 151 -see(Socrates, Mary) 152 153 all x.(ostrich(x) -> bird(x)) 154 bird(Tweety) 155 -ostrich(Sam) 156 Sam != Tweety 157 + all x.(bird(x) -> (ostrich(x) | x=Tweety)) 158 ------------------- 159 -bird(Sam) 160 """
161 - def assumptions(self):
162 assumptions = self._proverCommand.assumptions() 163 164 predicates = self._make_predicate_dict(assumptions) 165 166 assumptions2 = [] 167 for p,predHolder in predicates.iteritems(): 168 new_sig = self._make_unique_signature(predHolder) 169 new_sig_exs = [IndividualVariableExpression(v) for v in new_sig] 170 171 disjuncts = [] 172 for sig in predHolder.signatures: 173 equality_exs = [] 174 for v1,v2 in zip(new_sig_exs, sig): 175 equality_exs.append(EqualityExpression(v1,v2)) 176 disjuncts.append(reduce(Expression.__and__, equality_exs)) 177 178 for prop in predHolder.properties: 179 #replace variables from the signature with new sig variables 180 bindings = {} 181 for v1,v2 in zip(new_sig_exs, prop[0]): 182 bindings[v2] = v1 183 disjuncts.append(prop[1].substitute_bindings(bindings)) 184 185 #make the implication 186 antecedent = self._make_antecedent(p, new_sig) 187 consequent = reduce(Expression.__or__, disjuncts) 188 accum = ImpExpression(antecedent, consequent) 189 190 #quantify the implication 191 for new_sig_var in new_sig[::-1]: 192 accum = AllExpression(new_sig_var, accum) 193 assumptions2.append(accum) 194 195 return assumptions + assumptions2
196
197 - def _make_unique_signature(self, predHolder):
198 """ 199 This method figures out how many arguments the predicate takes and 200 returns a tuple containing that number of unique variables. 201 """ 202 return tuple([unique_variable() 203 for i in range(predHolder.signature_len)])
204
205 - def _make_antecedent(self, predicate, signature):
206 antecedent = predicate 207 for v in signature: 208 antecedent = antecedent(IndividualVariableExpression(v)) 209 return antecedent
210
211 - def _make_predicate_dict(self, assumptions):
212 """ 213 Create a dictionary of predicates from the assumptions. 214 215 @param assumptions: a C{list} of C{Expression}s 216 @return: C{dict} mapping C{VariableExpression}s to of C{PredHolder}s 217 """ 218 predicates = defaultdict(PredHolder) 219 for a in assumptions: 220 self._map_predicates(a, predicates) 221 return predicates
222
223 - def _map_predicates(self, expression, predDict):
224 if isinstance(expression, ApplicationExpression): 225 (func, args) = expression.uncurry() 226 if isinstance(func, VariableExpression): 227 predDict[func].append_sig(tuple(args)) 228 elif isinstance(expression, AndExpression): 229 self._map_predicates(expression.first, predDict) 230 self._map_predicates(expression.second, predDict) 231 elif isinstance(expression, AllExpression): 232 #collect all the universally quantified variables 233 sig = [expression.variable] 234 term = expression.term 235 while isinstance(term, AllExpression): 236 sig.append(term.variable) 237 term = term.term 238 if isinstance(term, ImpExpression): 239 if isinstance(term.second, ApplicationExpression): 240 func = term.second.function 241 if isinstance(func, VariableExpression): 242 predDict[func].append_prop((tuple(sig), term.first))
243
244 - def goal(self):
245 return self._proverCommand.goal()
246 247
248 -class PredHolder(object):
249 """ 250 This class will be used by a dictionary that will store information 251 about predicates to be used by the C{ClosedWorldProver}. 252 253 The 'signatures' property is a list of tuples defining signatures for 254 which the predicate is true. For instance, 'see(john, mary)' would be 255 result in the signature '(john,mary)' for 'see'. 256 257 The second element of the pair is a list of pairs such that the first 258 element of the pair is a tuple of variables and the second element is an 259 expression of those variables that makes the predicate true. For instance, 260 'all x.all y.(see(x,y) -> know(x,y))' would result in "((x,y),('see(x,y)'))" 261 for 'know'. 262 """
263 - def __init__(self):
264 self.signatures = [] 265 self.properties = [] 266 self.signature_len = None
267
268 - def append_sig(self, new_sig):
269 self.validate_sig_len(new_sig) 270 self.signatures.append(new_sig)
271
272 - def append_prop(self, new_prop):
273 self.validate_sig_len(new_prop[0]) 274 self.properties.append(new_prop)
275
276 - def validate_sig_len(self, new_sig):
277 if self.signature_len is None: 278 self.signature_len = len(new_sig) 279 elif self.signature_len != len(new_sig): 280 raise Exception("Signature lengths do not match")
281
282 - def __str__(self):
283 return '(%s,%s,%s)' % (self.signatures, self.properties, 284 self.signature_len)
285
286 - def __repr__(self):
287 return str(self)
288
289 -def closed_domain_demo():
290 lp = LogicParser() 291 292 p1 = lp.parse(r'exists x.walk(x)') 293 p2 = lp.parse(r'man(Socrates)') 294 c = lp.parse(r'walk(Socrates)') 295 prover = inference.get_prover(c, [p1,p2]) 296 print prover.prove() 297 cdp = ClosedDomainProver(prover) 298 for a in cdp.assumptions(): print a 299 print cdp.prove() 300 301 p1 = lp.parse(r'exists x.walk(x)') 302 p2 = lp.parse(r'man(Socrates)') 303 p3 = lp.parse(r'-walk(Bill)') 304 c = lp.parse(r'walk(Socrates)') 305 prover = inference.get_prover(c, [p1,p2,p3]) 306 print prover.prove() 307 cdp = ClosedDomainProver(prover) 308 for a in cdp.assumptions(): print a 309 print cdp.prove()
310
311 -def unique_names_demo():
312 lp = LogicParser() 313 314 p1 = lp.parse(r'man(Socrates)') 315 p2 = lp.parse(r'man(Bill)') 316 c = lp.parse(r'exists x.exists y.(x != y)') 317 prover = inference.get_prover(c, [p1,p2]) 318 print prover.prove() 319 unp = UniqueNamesProver(prover) 320 for a in unp.assumptions(): print a 321 print unp.prove() 322 323 p1 = lp.parse(r'all x.(walk(x) -> (x = Socrates))') 324 p2 = lp.parse(r'Bill = William') 325 p3 = lp.parse(r'Bill = Billy') 326 c = lp.parse(r'-walk(William)') 327 prover = inference.get_prover(c, [p1,p2,p3]) 328 print prover.prove() 329 unp = UniqueNamesProver(prover) 330 for a in unp.assumptions(): print a 331 print unp.prove()
332
333 -def closed_world_demo():
334 lp = LogicParser() 335 336 p1 = lp.parse(r'walk(Socrates)') 337 p2 = lp.parse(r'(Socrates != Bill)') 338 c = lp.parse(r'-walk(Bill)') 339 prover = inference.get_prover(c, [p1,p2]) 340 print prover.prove() 341 cwp = ClosedWorldProver(prover) 342 for a in cwp.assumptions(): print a 343 print cwp.prove() 344 345 p1 = lp.parse(r'see(Socrates, John)') 346 p2 = lp.parse(r'see(John, Mary)') 347 p3 = lp.parse(r'(Socrates != John)') 348 p4 = lp.parse(r'(John != Mary)') 349 c = lp.parse(r'-see(Socrates, Mary)') 350 prover = inference.get_prover(c, [p1,p2,p3,p4]) 351 print prover.prove() 352 cwp = ClosedWorldProver(prover) 353 for a in cwp.assumptions(): print a 354 print cwp.prove() 355 356 p1 = lp.parse(r'all x.(ostrich(x) -> bird(x))') 357 p2 = lp.parse(r'bird(Tweety)') 358 p3 = lp.parse(r'-ostrich(Sam)') 359 p4 = lp.parse(r'Sam != Tweety') 360 c = lp.parse(r'-bird(Sam)') 361 prover = inference.get_prover(c, [p1,p2,p3,p4]) 362 print prover.prove() 363 cwp = ClosedWorldProver(prover) 364 for a in cwp.assumptions(): print a 365 print cwp.prove()
366
367 -def combination_prover_demo():
368 lp = LogicParser() 369 370 p1 = lp.parse(r'see(Socrates, John)') 371 p2 = lp.parse(r'see(John, Mary)') 372 c = lp.parse(r'-see(Socrates, Mary)') 373 prover = inference.get_prover(c, [p1,p2]) 374 print prover.prove() 375 command = ClosedDomainProver( 376 UniqueNamesProver( 377 ClosedWorldProver(prover))) 378 for a in command.assumptions(): print a 379 print command.prove()
380 381 if __name__ == '__main__': 382 closed_domain_demo() 383 unique_names_demo() 384 closed_world_demo() 385 combination_prover_demo() 386