1# Natural Language Toolkit: Nonmonotonic Reasoning 2# 3# Author: Daniel H. Garrette <dhgarrette@gmail.com> 4# 5# Copyright (C) 2001-2019 NLTK Project 6# URL: <http://nltk.org> 7# For license information, see LICENSE.TXT 8 9""" 10A module to perform nonmonotonic reasoning. The ideas and demonstrations in 11this module are based on "Logical Foundations of Artificial Intelligence" by 12Michael R. Genesereth and Nils J. Nilsson. 13""" 14from __future__ import print_function, unicode_literals 15 16from collections import defaultdict 17from functools import reduce 18 19from nltk.inference.prover9 import Prover9, Prover9Command 20from nltk.sem.logic import ( 21 VariableExpression, 22 EqualityExpression, 23 ApplicationExpression, 24 Expression, 25 AbstractVariableExpression, 26 AllExpression, 27 BooleanExpression, 28 NegatedExpression, 29 ExistsExpression, 30 Variable, 31 ImpExpression, 32 AndExpression, 33 unique_variable, 34 operator, 35) 36 37from nltk.inference.api import Prover, ProverCommandDecorator 38from nltk.compat import python_2_unicode_compatible 39 40 41class ProverParseError(Exception): 42 pass 43 44 45def get_domain(goal, assumptions): 46 if goal is None: 47 all_expressions = assumptions 48 else: 49 all_expressions = assumptions + [-goal] 50 return reduce(operator.or_, (a.constants() for a in all_expressions), set()) 51 52 53class ClosedDomainProver(ProverCommandDecorator): 54 """ 55 This is a prover decorator that adds domain closure assumptions before 56 proving. 57 """ 58 59 def assumptions(self): 60 assumptions = [a for a in self._command.assumptions()] 61 goal = self._command.goal() 62 domain = get_domain(goal, assumptions) 63 return [self.replace_quants(ex, domain) for ex in assumptions] 64 65 def goal(self): 66 goal = self._command.goal() 67 domain = get_domain(goal, self._command.assumptions()) 68 return self.replace_quants(goal, domain) 69 70 def replace_quants(self, ex, domain): 71 """ 72 Apply the closed domain assumption to the expression 73 - Domain = union([e.free()|e.constants() for e in all_expressions]) 74 - translate "exists x.P" to "(z=d1 | z=d2 | ... ) & P.replace(x,z)" OR 75 "P.replace(x, d1) | P.replace(x, d2) | ..." 76 - translate "all x.P" to "P.replace(x, d1) & P.replace(x, d2) & ..." 77 :param ex: ``Expression`` 78 :param domain: set of {Variable}s 79 :return: ``Expression`` 80 """ 81 if isinstance(ex, AllExpression): 82 conjuncts = [ 83 ex.term.replace(ex.variable, VariableExpression(d)) for d in domain 84 ] 85 conjuncts = [self.replace_quants(c, domain) for c in conjuncts] 86 return reduce(lambda x, y: x & y, conjuncts) 87 elif isinstance(ex, BooleanExpression): 88 return ex.__class__( 89 self.replace_quants(ex.first, domain), 90 self.replace_quants(ex.second, domain), 91 ) 92 elif isinstance(ex, NegatedExpression): 93 return -self.replace_quants(ex.term, domain) 94 elif isinstance(ex, ExistsExpression): 95 disjuncts = [ 96 ex.term.replace(ex.variable, VariableExpression(d)) for d in domain 97 ] 98 disjuncts = [self.replace_quants(d, domain) for d in disjuncts] 99 return reduce(lambda x, y: x | y, disjuncts) 100 else: 101 return ex 102 103 104class UniqueNamesProver(ProverCommandDecorator): 105 """ 106 This is a prover decorator that adds unique names assumptions before 107 proving. 108 """ 109 110 def assumptions(self): 111 """ 112 - Domain = union([e.free()|e.constants() for e in all_expressions]) 113 - if "d1 = d2" cannot be proven from the premises, then add "d1 != d2" 114 """ 115 assumptions = self._command.assumptions() 116 117 domain = list(get_domain(self._command.goal(), assumptions)) 118 119 # build a dictionary of obvious equalities 120 eq_sets = SetHolder() 121 for a in assumptions: 122 if isinstance(a, EqualityExpression): 123 av = a.first.variable 124 bv = a.second.variable 125 # put 'a' and 'b' in the same set 126 eq_sets[av].add(bv) 127 128 new_assumptions = [] 129 for i, a in enumerate(domain): 130 for b in domain[i + 1 :]: 131 # if a and b are not already in the same equality set 132 if b not in eq_sets[a]: 133 newEqEx = EqualityExpression( 134 VariableExpression(a), VariableExpression(b) 135 ) 136 if Prover9().prove(newEqEx, assumptions): 137 # we can prove that the names are the same entity. 138 # remember that they are equal so we don't re-check. 139 eq_sets[a].add(b) 140 else: 141 # we can't prove it, so assume unique names 142 new_assumptions.append(-newEqEx) 143 144 return assumptions + new_assumptions 145 146 147class SetHolder(list): 148 """ 149 A list of sets of Variables. 150 """ 151 152 def __getitem__(self, item): 153 """ 154 :param item: ``Variable`` 155 :return: the set containing 'item' 156 """ 157 assert isinstance(item, Variable) 158 for s in self: 159 if item in s: 160 return s 161 # item is not found in any existing set. so create a new set 162 new = set([item]) 163 self.append(new) 164 return new 165 166 167class ClosedWorldProver(ProverCommandDecorator): 168 """ 169 This is a prover decorator that completes predicates before proving. 170 171 If the assumptions contain "P(A)", then "all x.(P(x) -> (x=A))" is the completion of "P". 172 If the assumptions contain "all x.(ostrich(x) -> bird(x))", then "all x.(bird(x) -> ostrich(x))" is the completion of "bird". 173 If the assumptions don't contain anything that are "P", then "all x.-P(x)" is the completion of "P". 174 175 walk(Socrates) 176 Socrates != Bill 177 + all x.(walk(x) -> (x=Socrates)) 178 ---------------- 179 -walk(Bill) 180 181 see(Socrates, John) 182 see(John, Mary) 183 Socrates != John 184 John != Mary 185 + all x.all y.(see(x,y) -> ((x=Socrates & y=John) | (x=John & y=Mary))) 186 ---------------- 187 -see(Socrates, Mary) 188 189 all x.(ostrich(x) -> bird(x)) 190 bird(Tweety) 191 -ostrich(Sam) 192 Sam != Tweety 193 + all x.(bird(x) -> (ostrich(x) | x=Tweety)) 194 + all x.-ostrich(x) 195 ------------------- 196 -bird(Sam) 197 """ 198 199 def assumptions(self): 200 assumptions = self._command.assumptions() 201 202 predicates = self._make_predicate_dict(assumptions) 203 204 new_assumptions = [] 205 for p in predicates: 206 predHolder = predicates[p] 207 new_sig = self._make_unique_signature(predHolder) 208 new_sig_exs = [VariableExpression(v) for v in new_sig] 209 210 disjuncts = [] 211 212 # Turn the signatures into disjuncts 213 for sig in predHolder.signatures: 214 equality_exs = [] 215 for v1, v2 in zip(new_sig_exs, sig): 216 equality_exs.append(EqualityExpression(v1, v2)) 217 disjuncts.append(reduce(lambda x, y: x & y, equality_exs)) 218 219 # Turn the properties into disjuncts 220 for prop in predHolder.properties: 221 # replace variables from the signature with new sig variables 222 bindings = {} 223 for v1, v2 in zip(new_sig_exs, prop[0]): 224 bindings[v2] = v1 225 disjuncts.append(prop[1].substitute_bindings(bindings)) 226 227 # make the assumption 228 if disjuncts: 229 # disjuncts exist, so make an implication 230 antecedent = self._make_antecedent(p, new_sig) 231 consequent = reduce(lambda x, y: x | y, disjuncts) 232 accum = ImpExpression(antecedent, consequent) 233 else: 234 # nothing has property 'p' 235 accum = NegatedExpression(self._make_antecedent(p, new_sig)) 236 237 # quantify the implication 238 for new_sig_var in new_sig[::-1]: 239 accum = AllExpression(new_sig_var, accum) 240 new_assumptions.append(accum) 241 242 return assumptions + new_assumptions 243 244 def _make_unique_signature(self, predHolder): 245 """ 246 This method figures out how many arguments the predicate takes and 247 returns a tuple containing that number of unique variables. 248 """ 249 return tuple(unique_variable() for i in range(predHolder.signature_len)) 250 251 def _make_antecedent(self, predicate, signature): 252 """ 253 Return an application expression with 'predicate' as the predicate 254 and 'signature' as the list of arguments. 255 """ 256 antecedent = predicate 257 for v in signature: 258 antecedent = antecedent(VariableExpression(v)) 259 return antecedent 260 261 def _make_predicate_dict(self, assumptions): 262 """ 263 Create a dictionary of predicates from the assumptions. 264 265 :param assumptions: a list of ``Expression``s 266 :return: dict mapping ``AbstractVariableExpression`` to ``PredHolder`` 267 """ 268 predicates = defaultdict(PredHolder) 269 for a in assumptions: 270 self._map_predicates(a, predicates) 271 return predicates 272 273 def _map_predicates(self, expression, predDict): 274 if isinstance(expression, ApplicationExpression): 275 func, args = expression.uncurry() 276 if isinstance(func, AbstractVariableExpression): 277 predDict[func].append_sig(tuple(args)) 278 elif isinstance(expression, AndExpression): 279 self._map_predicates(expression.first, predDict) 280 self._map_predicates(expression.second, predDict) 281 elif isinstance(expression, AllExpression): 282 # collect all the universally quantified variables 283 sig = [expression.variable] 284 term = expression.term 285 while isinstance(term, AllExpression): 286 sig.append(term.variable) 287 term = term.term 288 if isinstance(term, ImpExpression): 289 if isinstance(term.first, ApplicationExpression) and isinstance( 290 term.second, ApplicationExpression 291 ): 292 func1, args1 = term.first.uncurry() 293 func2, args2 = term.second.uncurry() 294 if ( 295 isinstance(func1, AbstractVariableExpression) 296 and isinstance(func2, AbstractVariableExpression) 297 and sig == [v.variable for v in args1] 298 and sig == [v.variable for v in args2] 299 ): 300 predDict[func2].append_prop((tuple(sig), term.first)) 301 predDict[func1].validate_sig_len(sig) 302 303 304@python_2_unicode_compatible 305class PredHolder(object): 306 """ 307 This class will be used by a dictionary that will store information 308 about predicates to be used by the ``ClosedWorldProver``. 309 310 The 'signatures' property is a list of tuples defining signatures for 311 which the predicate is true. For instance, 'see(john, mary)' would be 312 result in the signature '(john,mary)' for 'see'. 313 314 The second element of the pair is a list of pairs such that the first 315 element of the pair is a tuple of variables and the second element is an 316 expression of those variables that makes the predicate true. For instance, 317 'all x.all y.(see(x,y) -> know(x,y))' would result in "((x,y),('see(x,y)'))" 318 for 'know'. 319 """ 320 321 def __init__(self): 322 self.signatures = [] 323 self.properties = [] 324 self.signature_len = None 325 326 def append_sig(self, new_sig): 327 self.validate_sig_len(new_sig) 328 self.signatures.append(new_sig) 329 330 def append_prop(self, new_prop): 331 self.validate_sig_len(new_prop[0]) 332 self.properties.append(new_prop) 333 334 def validate_sig_len(self, new_sig): 335 if self.signature_len is None: 336 self.signature_len = len(new_sig) 337 elif self.signature_len != len(new_sig): 338 raise Exception("Signature lengths do not match") 339 340 def __str__(self): 341 return '(%s,%s,%s)' % (self.signatures, self.properties, self.signature_len) 342 343 def __repr__(self): 344 return "%s" % self 345 346 347def closed_domain_demo(): 348 lexpr = Expression.fromstring 349 350 p1 = lexpr(r'exists x.walk(x)') 351 p2 = lexpr(r'man(Socrates)') 352 c = lexpr(r'walk(Socrates)') 353 prover = Prover9Command(c, [p1, p2]) 354 print(prover.prove()) 355 cdp = ClosedDomainProver(prover) 356 print('assumptions:') 357 for a in cdp.assumptions(): 358 print(' ', a) 359 print('goal:', cdp.goal()) 360 print(cdp.prove()) 361 362 p1 = lexpr(r'exists x.walk(x)') 363 p2 = lexpr(r'man(Socrates)') 364 p3 = lexpr(r'-walk(Bill)') 365 c = lexpr(r'walk(Socrates)') 366 prover = Prover9Command(c, [p1, p2, p3]) 367 print(prover.prove()) 368 cdp = ClosedDomainProver(prover) 369 print('assumptions:') 370 for a in cdp.assumptions(): 371 print(' ', a) 372 print('goal:', cdp.goal()) 373 print(cdp.prove()) 374 375 p1 = lexpr(r'exists x.walk(x)') 376 p2 = lexpr(r'man(Socrates)') 377 p3 = lexpr(r'-walk(Bill)') 378 c = lexpr(r'walk(Socrates)') 379 prover = Prover9Command(c, [p1, p2, p3]) 380 print(prover.prove()) 381 cdp = ClosedDomainProver(prover) 382 print('assumptions:') 383 for a in cdp.assumptions(): 384 print(' ', a) 385 print('goal:', cdp.goal()) 386 print(cdp.prove()) 387 388 p1 = lexpr(r'walk(Socrates)') 389 p2 = lexpr(r'walk(Bill)') 390 c = lexpr(r'all x.walk(x)') 391 prover = Prover9Command(c, [p1, p2]) 392 print(prover.prove()) 393 cdp = ClosedDomainProver(prover) 394 print('assumptions:') 395 for a in cdp.assumptions(): 396 print(' ', a) 397 print('goal:', cdp.goal()) 398 print(cdp.prove()) 399 400 p1 = lexpr(r'girl(mary)') 401 p2 = lexpr(r'dog(rover)') 402 p3 = lexpr(r'all x.(girl(x) -> -dog(x))') 403 p4 = lexpr(r'all x.(dog(x) -> -girl(x))') 404 p5 = lexpr(r'chase(mary, rover)') 405 c = lexpr(r'exists y.(dog(y) & all x.(girl(x) -> chase(x,y)))') 406 prover = Prover9Command(c, [p1, p2, p3, p4, p5]) 407 print(prover.prove()) 408 cdp = ClosedDomainProver(prover) 409 print('assumptions:') 410 for a in cdp.assumptions(): 411 print(' ', a) 412 print('goal:', cdp.goal()) 413 print(cdp.prove()) 414 415 416def unique_names_demo(): 417 lexpr = Expression.fromstring 418 419 p1 = lexpr(r'man(Socrates)') 420 p2 = lexpr(r'man(Bill)') 421 c = lexpr(r'exists x.exists y.(x != y)') 422 prover = Prover9Command(c, [p1, p2]) 423 print(prover.prove()) 424 unp = UniqueNamesProver(prover) 425 print('assumptions:') 426 for a in unp.assumptions(): 427 print(' ', a) 428 print('goal:', unp.goal()) 429 print(unp.prove()) 430 431 p1 = lexpr(r'all x.(walk(x) -> (x = Socrates))') 432 p2 = lexpr(r'Bill = William') 433 p3 = lexpr(r'Bill = Billy') 434 c = lexpr(r'-walk(William)') 435 prover = Prover9Command(c, [p1, p2, p3]) 436 print(prover.prove()) 437 unp = UniqueNamesProver(prover) 438 print('assumptions:') 439 for a in unp.assumptions(): 440 print(' ', a) 441 print('goal:', unp.goal()) 442 print(unp.prove()) 443 444 445def closed_world_demo(): 446 lexpr = Expression.fromstring 447 448 p1 = lexpr(r'walk(Socrates)') 449 p2 = lexpr(r'(Socrates != Bill)') 450 c = lexpr(r'-walk(Bill)') 451 prover = Prover9Command(c, [p1, p2]) 452 print(prover.prove()) 453 cwp = ClosedWorldProver(prover) 454 print('assumptions:') 455 for a in cwp.assumptions(): 456 print(' ', a) 457 print('goal:', cwp.goal()) 458 print(cwp.prove()) 459 460 p1 = lexpr(r'see(Socrates, John)') 461 p2 = lexpr(r'see(John, Mary)') 462 p3 = lexpr(r'(Socrates != John)') 463 p4 = lexpr(r'(John != Mary)') 464 c = lexpr(r'-see(Socrates, Mary)') 465 prover = Prover9Command(c, [p1, p2, p3, p4]) 466 print(prover.prove()) 467 cwp = ClosedWorldProver(prover) 468 print('assumptions:') 469 for a in cwp.assumptions(): 470 print(' ', a) 471 print('goal:', cwp.goal()) 472 print(cwp.prove()) 473 474 p1 = lexpr(r'all x.(ostrich(x) -> bird(x))') 475 p2 = lexpr(r'bird(Tweety)') 476 p3 = lexpr(r'-ostrich(Sam)') 477 p4 = lexpr(r'Sam != Tweety') 478 c = lexpr(r'-bird(Sam)') 479 prover = Prover9Command(c, [p1, p2, p3, p4]) 480 print(prover.prove()) 481 cwp = ClosedWorldProver(prover) 482 print('assumptions:') 483 for a in cwp.assumptions(): 484 print(' ', a) 485 print('goal:', cwp.goal()) 486 print(cwp.prove()) 487 488 489def combination_prover_demo(): 490 lexpr = Expression.fromstring 491 492 p1 = lexpr(r'see(Socrates, John)') 493 p2 = lexpr(r'see(John, Mary)') 494 c = lexpr(r'-see(Socrates, Mary)') 495 prover = Prover9Command(c, [p1, p2]) 496 print(prover.prove()) 497 command = ClosedDomainProver(UniqueNamesProver(ClosedWorldProver(prover))) 498 for a in command.assumptions(): 499 print(a) 500 print(command.prove()) 501 502 503def default_reasoning_demo(): 504 lexpr = Expression.fromstring 505 506 premises = [] 507 508 # define taxonomy 509 premises.append(lexpr(r'all x.(elephant(x) -> animal(x))')) 510 premises.append(lexpr(r'all x.(bird(x) -> animal(x))')) 511 premises.append(lexpr(r'all x.(dove(x) -> bird(x))')) 512 premises.append(lexpr(r'all x.(ostrich(x) -> bird(x))')) 513 premises.append(lexpr(r'all x.(flying_ostrich(x) -> ostrich(x))')) 514 515 # default properties 516 premises.append( 517 lexpr(r'all x.((animal(x) & -Ab1(x)) -> -fly(x))') 518 ) # normal animals don't fly 519 premises.append( 520 lexpr(r'all x.((bird(x) & -Ab2(x)) -> fly(x))') 521 ) # normal birds fly 522 premises.append( 523 lexpr(r'all x.((ostrich(x) & -Ab3(x)) -> -fly(x))') 524 ) # normal ostriches don't fly 525 526 # specify abnormal entities 527 premises.append(lexpr(r'all x.(bird(x) -> Ab1(x))')) # flight 528 premises.append(lexpr(r'all x.(ostrich(x) -> Ab2(x))')) # non-flying bird 529 premises.append(lexpr(r'all x.(flying_ostrich(x) -> Ab3(x))')) # flying ostrich 530 531 # define entities 532 premises.append(lexpr(r'elephant(E)')) 533 premises.append(lexpr(r'dove(D)')) 534 premises.append(lexpr(r'ostrich(O)')) 535 536 # print the assumptions 537 prover = Prover9Command(None, premises) 538 command = UniqueNamesProver(ClosedWorldProver(prover)) 539 for a in command.assumptions(): 540 print(a) 541 542 print_proof('-fly(E)', premises) 543 print_proof('fly(D)', premises) 544 print_proof('-fly(O)', premises) 545 546 547def print_proof(goal, premises): 548 lexpr = Expression.fromstring 549 prover = Prover9Command(lexpr(goal), premises) 550 command = UniqueNamesProver(ClosedWorldProver(prover)) 551 print(goal, prover.prove(), command.prove()) 552 553 554def demo(): 555 closed_domain_demo() 556 unique_names_demo() 557 closed_world_demo() 558 combination_prover_demo() 559 default_reasoning_demo() 560 561 562if __name__ == '__main__': 563 demo() 564