nltk.inference.resolution

1 # Natural Language Toolkit: First-order Resolution-based Theorem Prover 2 # 3 # Author: Dan 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 from nltk.sem.logic import * 10 from nltk.internals import Counter 11 from nltk.inference.api import Prover, ProverCommand 12 from nltk import defaultdict 13 14 """ 15 Module for a resolution-based First Order theorem prover. 16 """ 17 18 _skolem_function_counter = Counter() 19

20 -class ProverParseError(Exception): pass

21

22 -class Resolution(Prover):

23 ANSWER_KEY = 'ANSWER' 24 _assume_false=True 25

26 - def prove(self, goal=None, assumptions=[], verbose=False):

27 """ 28 @param goal: Input expression to prove 29 @type goal: L{logic.Expression} 30 @param assumptions: Input expressions to use as assumptions in the proof 31 @type assumptions: L{list} of logic.Expression objects 32 """ 33 result = None 34 try: 35 clauses = [] 36 if goal: 37 clauses.extend(clausify(-goal)) 38 for a in assumptions: 39 clauses.extend(clausify(a)) 40 result, proof = self._attempt_proof(clauses) 41 except RuntimeError, e: 42 if self._assume_false and str(e).startswith('maximum recursion depth exceeded'): 43 result = False 44 proof = '' 45 else: 46 if verbose: 47 print e 48 else: 49 raise e 50 return (result, proof)

51

52 - def _attempt_proof(self, clauses):

53 #map indices to lists of indices, to store attempted unifications 54 tried = defaultdict(list) 55 56 i = 0 57 while i < len(clauses): 58 if not clauses[i].is_tautology(): 59 #since we try clauses in order, we should start after the last 60 #index tried 61 if tried[i]: 62 j = tried[i][-1] + 1 63 else: 64 j = i + 1 #nothing tried yet for 'i', so start with the next 65 66 while j < len(clauses): 67 #don't: 1) unify a clause with itself, 68 # 2) use tautologies 69 if i != j and j and not clauses[j].is_tautology(): 70 tried[i].append(j) 71 newclauses = clauses[i].unify(clauses[j]) 72 if newclauses: 73 for newclause in newclauses: 74 newclause._parents = (i+1, j+1) 75 clauses.append(newclause) 76 if not len(newclause): #if there's an empty clause 77 return (True, clauses) 78 i=-1 #since we added a new clause, restart from the top 79 break 80 j += 1 81 i += 1 82 return (False, clauses)

83

84 -class ResolutionCommand(ProverCommand):

85 - def __init__(self, goal=None, assumptions=[]):

86 """ 87 @param goal: Input expression to prove 88 @type goal: L{logic.Expression} 89 @param assumptions: Input expressions to use as assumptions in 90 the proof. 91 @type assumptions: C{list} of L{logic.Expression} 92 """ 93 ProverCommand.__init__(self, Resolution(), goal, assumptions) 94 self._clauses = None

95

96 - def prove(self, verbose=False):

97 """ 98 Perform the actual proof. Store the result to prevent unnecessary 99 re-proving. 100 """ 101 if self._result is None: 102 self._result, clauses = self._prover.prove(self.goal(), 103 self.assumptions(), 104 verbose) 105 self._clauses = clauses 106 self._proof = self.decorate_proof(clauses) 107 return self._result

108

109 - def find_answers(self, verbose=False):

110 self.prove(verbose) 111 112 answers = set() 113 answer_ex = VariableExpression(Variable(Resolution.ANSWER_KEY)) 114 for clause in self._clauses: 115 for term in clause: 116 if isinstance(term, ApplicationExpression) and\ 117 term.function == answer_ex and\ 118 not isinstance(term.argument, IndividualVariableExpression): 119 answers.add(term.argument) 120 return answers

121

122 - def decorate_proof(self, clauses):

123 """ 124 Decorate the proof output. 125 """ 126 out = '' 127 max_clause_len = max([len(str(clause)) for clause in clauses]) 128 max_seq_len = len(str(len(clauses))) 129 for i in range(len(clauses)): 130 parents = 'A' 131 taut = '' 132 if clauses[i].is_tautology(): 133 taut = 'Tautology' 134 if clauses[i]._parents: 135 parents = str(clauses[i]._parents) 136 parents = ' '*(max_clause_len-len(str(clauses[i]))+1) + parents 137 seq = ' '*(max_seq_len-len(str(i+1))) + str(i+1) 138 out += '[%s] %s %s %s\n' % (seq, clauses[i], parents, taut) 139 return out

140

141 -class Clause(list):

142 - def __init__(self, data):

143 list.__init__(self, data) 144 self._is_tautology = None 145 self._parents = None

146

147 - def unify(self, other, bindings=None, used=None, skipped=None, debug=False):

148 """ 149 Attempt to unify this Clause with the other, returning a list of 150 resulting, unified, Clauses. 151 152 @param other: C{Clause} with which to unify 153 @param bindings: C{BindingDict} containing bindings that should be used 154 during the unification 155 @param used: C{tuple} of two C{list}s of atoms. The first lists the 156 atoms from 'self' that were successfully unified with atoms from 157 'other'. The second lists the atoms from 'other' that were successfully 158 unified with atoms from 'self'. 159 @param skipped: C{tuple} of two C{Clause}s. The first is a list of all 160 the atoms from the 'self' Clause that have not been unified with 161 anything on the path. The second is same thing for the 'other' Clause. 162 @param debug: C{bool} indicating whether debug statements should print 163 @return: C{list} containing all the resulting C{Clause}s that could be 164 obtained by unification 165 """ 166 if bindings is None: bindings = BindingDict() 167 if used is None: used = ([],[]) 168 if skipped is None: skipped = ([],[]) 169 if isinstance(debug, bool): debug = DebugObject(debug) 170 171 newclauses = _iterate_first(self, other, bindings, used, skipped, _complete_unify_path, debug) 172 173 #remove subsumed clauses. make a list of all indices of subsumed 174 #clauses, and then remove them from the list 175 subsumed = [] 176 for i, c1 in enumerate(newclauses): 177 if i not in subsumed: 178 for j, c2 in enumerate(newclauses): 179 if i!=j and j not in subsumed and c1.subsumes(c2): 180 subsumed.append(j) 181 result = [] 182 for i in range(len(newclauses)): 183 if i not in subsumed: 184 result.append(newclauses[i]) 185 186 return result

187

188 - def isSubsetOf(self, other):

189 """ 190 Return True iff every term in 'self' is a term in 'other'. 191 192 @param other: C{Clause} 193 @return: C{bool} 194 """ 195 for a in self: 196 if a not in other: 197 return False 198 return True

199

200 - def subsumes(self, other):

201 """ 202 Return True iff 'self' subsumes 'other', this is, if there is a 203 substitution such that every term in 'self' can be unified with a term 204 in 'other'. 205 206 @param other: C{Clause} 207 @return: C{bool} 208 """ 209 negatedother = [] 210 for atom in other: 211 if isinstance(atom, NegatedExpression): 212 negatedother.append(atom.term) 213 else: 214 negatedother.append(-atom) 215 216 negatedotherClause = Clause(negatedother) 217 218 bindings = BindingDict() 219 used = ([],[]) 220 skipped = ([],[]) 221 debug = DebugObject(False) 222 223 return len(_iterate_first(self, negatedotherClause, bindings, used, 224 skipped, _subsumes_finalize, 225 debug)) > 0

226

227 - def __getslice__(self, start, end):

228 return Clause(list.__getslice__(self, start, end))

229

230 - def __sub__(self, other):

231 return Clause([a for a in self if a not in other])

232

233 - def __add__(self, other):

234 return Clause(list.__add__(self, other))

235

236 - def is_tautology(self):

237 """ 238 Self is a tautology if it contains ground terms P and -P. The ground 239 term, P, must be an exact match, ie, not using unification. 240 """ 241 if self._is_tautology is not None: 242 return self._is_tautology 243 for i,a in enumerate(self): 244 if not isinstance(a, EqualityExpression): 245 j = len(self)-1 246 while j > i: 247 b = self[j] 248 if isinstance(a, NegatedExpression): 249 if a.term == b: 250 self._is_tautology = True 251 return True 252 elif isinstance(b, NegatedExpression): 253 if a == b.term: 254 self._is_tautology = True 255 return True 256 j -= 1 257 self._is_tautology = False 258 return False

259

260 - def free(self):

261 s = set() 262 for atom in self: 263 s |= atom.free(False) 264 return s

265

266 - def replace(self, variable, expression):

267 """ 268 Replace every instance of variable with expression across every atom 269 in the clause 270 271 @param variable: C{Variable} 272 @param expression: C{Expression} 273 """ 274 return Clause([atom.replace(variable, expression) for atom in self])

275

276 - def substitute_bindings(self, bindings):

277 """ 278 Replace every binding 279 280 @param bindings: A C{list} of tuples mapping VariableExpressions to the 281 Expressions to which they are bound 282 @return: C{Clause} 283 """ 284 return Clause([atom.substitute_bindings(bindings) for atom in self])

285

286 - def __str__(self):

287 return '{' + ', '.join([str(item) for item in self]) + '}'

288

289 - def __repr__(self):

290 return str(self)

291

292 -def _iterate_first(first, second, bindings, used, skipped, finalize_method, debug):

293 """ 294 This method facilitates movement through the terms of 'self' 295 """ 296 debug.line('unify(%s,%s) %s'%(first, second, bindings)) 297 298 if not len(first) or not len(second): #if no more recursions can be performed 299 return finalize_method(first, second, bindings, used, skipped, debug) 300 else: 301 #explore this 'self' atom 302 result = _iterate_second(first, second, bindings, used, skipped, finalize_method, debug+1) 303 304 #skip this possible 'self' atom 305 newskipped = (skipped[0]+[first[0]], skipped[1]) 306 result += _iterate_first(first[1:], second, bindings, used, newskipped, finalize_method, debug+1) 307 308 try: 309 newbindings, newused, unused = _unify_terms(first[0], second[0], bindings, used) 310 #Unification found, so progress with this line of unification 311 #put skipped and unused terms back into play for later unification. 312 newfirst = first[1:] + skipped[0] + unused[0] 313 newsecond = second[1:] + skipped[1] + unused[1] 314 result += _iterate_first(newfirst, newsecond, newbindings, newused, ([],[]), finalize_method, debug+1) 315 except BindingException: 316 #the atoms could not be unified, 317 pass 318 319 return result

320

321 -def _iterate_second(first, second, bindings, used, skipped, finalize_method, debug):

322 """ 323 This method facilitates movement through the terms of 'other' 324 """ 325 debug.line('unify(%s,%s) %s'%(first, second, bindings)) 326 327 if not len(first) or not len(second): #if no more recursions can be performed 328 return finalize_method(first, second, bindings, used, skipped, debug) 329 else: 330 #skip this possible pairing and move to the next 331 newskipped = (skipped[0], skipped[1]+[second[0]]) 332 result = _iterate_second(first, second[1:], bindings, used, newskipped, finalize_method, debug+1) 333 334 try: 335 newbindings, newused, unused = _unify_terms(first[0], second[0], bindings, used) 336 #Unification found, so progress with this line of unification 337 #put skipped and unused terms back into play for later unification. 338 newfirst = first[1:] + skipped[0] + unused[0] 339 newsecond = second[1:] + skipped[1] + unused[1] 340 result += _iterate_second(newfirst, newsecond, newbindings, newused, ([],[]), finalize_method, debug+1) 341 except BindingException: 342 #the atoms could not be unified, 343 pass 344 345 return result

346

347 -def _unify_terms(a, b, bindings=None, used=None):

348 """ 349 This method attempts to unify two terms. Two expressions are unifiable 350 if there exists a substitution function S such that S(a) == S(-b). 351 352 @param a: C{Expression} 353 @param b: C{Expression} 354 @param bindings: C{BindingDict} a starting set of bindings with which 355 the unification must be consistent 356 @return: C{BindingDict} A dictionary of the bindings required to unify 357 @raise C{BindingException}: If the terms cannot be unified 358 """ 359 assert isinstance(a, Expression) 360 assert isinstance(b, Expression) 361 362 if bindings is None: bindings = BindingDict() 363 if used is None: used = ([],[]) 364 365 # Use resolution 366 if isinstance(a, NegatedExpression) and isinstance(b, ApplicationExpression): 367 newbindings = most_general_unification(a.term, b, bindings) 368 newused = (used[0]+[a], used[1]+[b]) 369 unused = ([],[]) 370 elif isinstance(a, ApplicationExpression) and isinstance(b, NegatedExpression): 371 newbindings = most_general_unification(a, b.term, bindings) 372 newused = (used[0]+[a], used[1]+[b]) 373 unused = ([],[]) 374 375 # Use demodulation 376 elif isinstance(a, EqualityExpression): 377 newbindings = BindingDict([(a.first.variable, a.second)]) 378 newused = (used[0]+[a], used[1]) 379 unused = ([],[b]) 380 elif isinstance(b, EqualityExpression): 381 newbindings = BindingDict([(b.first.variable, b.second)]) 382 newused = (used[0], used[1]+[b]) 383 unused = ([a],[]) 384 385 else: 386 raise BindingException((a, b)) 387 388 return newbindings, newused, unused

389

390 -def _complete_unify_path(first, second, bindings, used, skipped, debug):

391 if used[0] or used[1]: #if bindings were made along the path 392 newclause = Clause(skipped[0] + skipped[1] + first + second) 393 debug.line(' -> New Clause: %s' % newclause) 394 return [newclause.substitute_bindings(bindings)] 395 else: #no bindings made means no unification occurred. so no result 396 debug.line(' -> End') 397 return []

398

399 -def _subsumes_finalize(first, second, bindings, used, skipped, debug):

400 if not len(skipped[0]) and not len(first): 401 #If there are no skipped terms and no terms left in 'first', then 402 #all of the terms in the original 'self' were unified with terms 403 #in 'other'. Therefore, there exists a binding (this one) such that 404 #every term in self can be unified with a term in other, which 405 #is the definition of subsumption. 406 return [True] 407 else: 408 return []

409

410 -def clausify(expression):

411 """ 412 Skolemize, clausify, and standardize the variables apart. 413 """ 414 clause_list = [] 415 for clause in _clausify(skolemize(expression)): 416 for free in clause.free(): 417 if is_indvar(free.name): 418 newvar = IndividualVariableExpression(unique_variable()) 419 clause = clause.replace(free, newvar) 420 clause_list.append(clause) 421 return clause_list

422

423 -def _clausify(expression):

424 """ 425 @param expression: a skolemized expression in CNF 426 """ 427 if isinstance(expression, AndExpression): 428 return _clausify(expression.first) + _clausify(expression.second) 429 elif isinstance(expression, OrExpression): 430 first = _clausify(expression.first) 431 second = _clausify(expression.second) 432 assert len(first) == 1 433 assert len(second) == 1 434 return [first[0] + second[0]] 435 elif isinstance(expression, EqualityExpression): 436 return [Clause([expression])] 437 elif isinstance(expression, ApplicationExpression): 438 return [Clause([expression])] 439 elif isinstance(expression, NegatedExpression): 440 if isinstance(expression.term, ApplicationExpression): 441 return [Clause([expression])] 442 elif isinstance(expression.term, EqualityExpression): 443 return [Clause([expression])] 444 raise ProverParseError()

445 446

447 -def skolemize(expression, univ_scope=None):

448 """ 449 Skolemize the expression and convert to conjunctive normal form (CNF) 450 """ 451 if univ_scope is None: 452 univ_scope = set() 453 454 if isinstance(expression, AllExpression): 455 term = skolemize(expression.term, univ_scope|set([expression.variable])) 456 return term.replace(expression.variable, IndividualVariableExpression(unique_variable())) 457 elif isinstance(expression, AndExpression): 458 return skolemize(expression.first, univ_scope) &\ 459 skolemize(expression.second, univ_scope) 460 elif isinstance(expression, OrExpression): 461 return to_cnf(skolemize(expression.first, univ_scope), 462 skolemize(expression.second, univ_scope)) 463 elif isinstance(expression, ImpExpression): 464 return to_cnf(skolemize(-expression.first, univ_scope), 465 skolemize(expression.second, univ_scope)) 466 elif isinstance(expression, IffExpression): 467 return to_cnf(skolemize(-expression.first, univ_scope), 468 skolemize(expression.second, univ_scope)) &\ 469 to_cnf(skolemize(expression.first, univ_scope), 470 skolemize(-expression.second, univ_scope)) 471 elif isinstance(expression, EqualityExpression): 472 return expression 473 elif isinstance(expression, NegatedExpression): 474 negated = expression.term 475 if isinstance(negated, AllExpression): 476 term = skolemize(-negated.term, univ_scope) 477 if univ_scope: 478 return term.replace(negated.variable, _get_skolem_function(univ_scope)) 479 else: 480 skolem_constant = IndividualVariableExpression(unique_variable()) 481 return term.replace(negated.variable, skolem_constant) 482 elif isinstance(negated, AndExpression): 483 return to_cnf(skolemize(-negated.first, univ_scope), 484 skolemize(-negated.second, univ_scope)) 485 elif isinstance(negated, OrExpression): 486 return skolemize(-negated.first, univ_scope) &\ 487 skolemize(-negated.second, univ_scope) 488 elif isinstance(negated, ImpExpression): 489 return skolemize(negated.first, univ_scope) &\ 490 skolemize(-negated.second, univ_scope) 491 elif isinstance(negated, IffExpression): 492 return to_cnf(skolemize(-negated.first, univ_scope), 493 skolemize(-negated.second, univ_scope)) &\ 494 to_cnf(skolemize(negated.first, univ_scope), 495 skolemize(negated.second, univ_scope)) 496 elif isinstance(negated, EqualityExpression): 497 return expression 498 elif isinstance(negated, NegatedExpression): 499 return skolemize(negated.term, univ_scope) 500 elif isinstance(negated, ExistsExpression): 501 term = skolemize(-negated.term, univ_scope|set([negated.variable])) 502 return term.replace(negated.variable, IndividualVariableExpression(unique_variable())) 503 elif isinstance(negated, ApplicationExpression): 504 return expression 505 else: 506 raise ProverParseError() 507 elif isinstance(expression, ExistsExpression): 508 term = skolemize(expression.term, univ_scope) 509 if univ_scope: 510 return term.replace(expression.variable, _get_skolem_function(univ_scope)) 511 else: 512 skolem_constant = IndividualVariableExpression(unique_variable()) 513 return term.replace(expression.variable, skolem_constant) 514 elif isinstance(expression, ApplicationExpression): 515 return expression 516 else: 517 raise ProverParseError()

518

519 -def to_cnf(first, second):

520 """ 521 Convert this split disjunction to conjunctive normal form (CNF) 522 """ 523 if isinstance(first, AndExpression): 524 r_first = to_cnf(first.first, second) 525 r_second = to_cnf(first.second, second) 526 return r_first & r_second 527 elif isinstance(second, AndExpression): 528 r_first = to_cnf(first, second.first) 529 r_second = to_cnf(first, second.second) 530 return r_first & r_second 531 else: 532 return first | second

533

534 -def _get_skolem_function(univ_scope):

535 """ 536 Return a skolem function over the varibles in univ_scope 537 """ 538 skolem_function = VariableExpression(Variable('F%s' % _skolem_function_counter.get())) 539 for v in list(univ_scope): 540 skolem_function = skolem_function(VariableExpression(v)) 541 return skolem_function

542 543

544 -class BindingDict(object):

545 - def __init__(self, binding_list=None):

546 """ 547 @param binding_list: C{list} of (C{VariableExpression}, C{AtomicExpression}) to initialize the dictionary 548 """ 549 self.d = {} 550 551 if binding_list: 552 for (v, b) in binding_list: 553 self[v] = b

554

555 - def __setitem__(self, variable, binding):

556 """ 557 A binding is consistent with the dict if its variable is not already bound, OR if its 558 variable is already bound to its argument. 559 560 @param variable: C{Variable} The variable to bind 561 @param binding: C{Expression} The atomic to which 'variable' should be bound 562 @raise BindingException: If the variable cannot be bound in this dictionary 563 """ 564 assert isinstance(variable, Variable) 565 assert isinstance(binding, Expression) 566 567 try: 568 existing = self[variable] 569 except KeyError: 570 existing = None 571 572 if not existing or binding == existing: 573 self.d[variable] = binding 574 elif isinstance(binding, IndividualVariableExpression): 575 # Since variable is already bound, try to bind binding to variable 576 try: 577 existing = self[binding.variable] 578 except KeyError: 579 existing = None 580 581 if is_indvar(variable.name): 582 binding2 = IndividualVariableExpression(variable) 583 else: 584 binding2 = VariableExpression(variable) 585 586 if not existing or binding2 == existing: 587 self.d[binding.variable] = binding2 588 else: 589 raise BindingException('Variable %s already bound to another ' 590 'value' % (variable)) 591 else: 592 raise BindingException('Variable %s already bound to another ' 593 'value' % (variable))

594

595 - def __getitem__(self, variable):

596 """ 597 Return the expression to which 'variable' is bound 598 """ 599 assert isinstance(variable, Variable) 600 601 intermediate = self.d[variable] 602 while intermediate: 603 try: 604 intermediate = self.d[intermediate] 605 except KeyError: 606 return intermediate

607

608 - def __contains__(self, item):

609 return item in self.d

610

611 - def __add__(self, other):

612 """ 613 @param other: C{BindingDict} The dict with which to combine self 614 @return: C{BindingDict} A new dict containing all the elements of both parameters 615 @raise BindingException: If the parameter dictionaries are not consistent with each other 616 """ 617 try: 618 combined = BindingDict() 619 for v in self.d: 620 combined[v] = self.d[v] 621 for v in other.d: 622 combined[v] = other.d[v] 623 return combined 624 except BindingException: 625 raise BindingException("Attempting to add two contradicting " 626 "BindingDicts: '%s' and '%s'" 627 % (self, other))

628

629 - def __len__(self):

630 return len(self.d)

631

632 - def __str__(self):

633 return '{' + ', '.join(['%s: %s' % (v, self.d[v]) for v in self.d]) + '}'

634

635 - def __repr__(self):

636 return str(self)

637 638

639 -def most_general_unification(a, b, bindings=None):

640 """ 641 Find the most general unification of the two given expressions 642 643 @param a: C{Expression} 644 @param b: C{Expression} 645 @param bindings: C{BindingDict} a starting set of bindings with which the 646 unification must be consistent 647 @return: a list of bindings 648 @raise BindingException: if the Expressions cannot be unified 649 """ 650 if bindings is None: 651 bindings = BindingDict() 652 653 if a == b: 654 return bindings 655 elif isinstance(a, VariableExpression) and is_indvar(a.variable.name): 656 return _mgu_var(a, b, bindings) 657 elif isinstance(b, VariableExpression) and is_indvar(b.variable.name): 658 return _mgu_var(b, a, bindings) 659 elif isinstance(a, ApplicationExpression) and\ 660 isinstance(b, ApplicationExpression): 661 return most_general_unification(a.function, b.function, bindings) +\ 662 most_general_unification(a.argument, b.argument, bindings) 663 raise BindingException((a, b))

664

665 -def _mgu_var(var, expression, bindings):

666 if var.variable in expression.free(False): 667 raise BindingException((var, expression)) 668 else: 669 return BindingDict([(var.variable, expression)]) + bindings

670 671

672 -class BindingException(Exception):

673 - def __init__(self, arg):

674 if isinstance(arg, tuple): 675 Exception.__init__(self, "'%s' cannot be bound to '%s'" % arg) 676 else: 677 Exception.__init__(self, arg)

678

679 -class UnificationException(Exception):

680 - def __init__(self, a, b):

681 Exception.__init__(self, "'%s' cannot unify with '%s'" % (a,b))

682 683

684 -class DebugObject(object):

685 - def __init__(self, enabled=True, indent=0):

686 self.enabled = enabled 687 self.indent = indent

688

689 - def __add__(self, i):

690 return DebugObject(self.enabled, self.indent+i)

691

692 - def line(self, line):

693 if self.enabled: 694 print ' '*self.indent + line

695 696

697 -def testResolution():

698 resolution_test(r'man(x)') 699 resolution_test(r'(man(x) -> man(x))') 700 resolution_test(r'(man(x) -> --man(x))') 701 resolution_test(r'-(man(x) and -man(x))') 702 resolution_test(r'(man(x) or -man(x))') 703 resolution_test(r'(man(x) -> man(x))') 704 resolution_test(r'-(man(x) and -man(x))') 705 resolution_test(r'(man(x) or -man(x))') 706 resolution_test(r'(man(x) -> man(x))') 707 resolution_test(r'(man(x) iff man(x))') 708 resolution_test(r'-(man(x) iff -man(x))') 709 resolution_test('all x.man(x)') 710 resolution_test('-all x.some y.F(x,y) & some x.all y.(-F(x,y))') 711 resolution_test('some x.all y.sees(x,y)') 712 713 p1 = LogicParser().parse(r'all x.(man(x) -> mortal(x))') 714 p2 = LogicParser().parse(r'man(Socrates)') 715 c = LogicParser().parse(r'mortal(Socrates)') 716 print '%s, %s |- %s: %s' % (p1, p2, c, ProverCommand(Resolution(), c, [p1,p2]).prove()) 717 718 p1 = LogicParser().parse(r'all x.(man(x) -> walks(x))') 719 p2 = LogicParser().parse(r'man(John)') 720 c = LogicParser().parse(r'some y.walks(y)') 721 print '%s, %s |- %s: %s' % (p1, p2, c, ProverCommand(Resolution(), c, [p1,p2]).prove()) 722 723 p = LogicParser().parse(r'some e1.some e2.(believe(e1,john,e2) & walk(e2,mary))') 724 c = LogicParser().parse(r'some e0.walk(e0,mary)') 725 print '%s |- %s: %s' % (p, c, ProverCommand(Resolution(), c, [p]).prove())

726

727 -def resolution_test(e):

728 f = LogicParser().parse(e) 729 t = ProverCommand(Resolution(), f) 730 print '|- %s: %s' % (f, t.prove())

731

732 -def test_clausify():

733 lp = LogicParser() 734 735 print clausify(lp.parse('P(x) | Q(x)')) 736 print clausify(lp.parse('(P(x) & Q(x)) | R(x)')) 737 print clausify(lp.parse('P(x) | (Q(x) & R(x))')) 738 print clausify(lp.parse('(P(x) & Q(x)) | (R(x) & S(x))')) 739 740 print clausify(lp.parse('P(x) | Q(x) | R(x)')) 741 print clausify(lp.parse('P(x) | (Q(x) & R(x)) | S(x)')) 742 743 print clausify(lp.parse('exists x.P(x) | Q(x)')) 744 745 print clausify(lp.parse('-(-P(x) & Q(x))')) 746 print clausify(lp.parse('P(x) <-> Q(x)')) 747 print clausify(lp.parse('-(P(x) <-> Q(x))')) 748 print clausify(lp.parse('-(all x.P(x))')) 749 print clausify(lp.parse('-(some x.P(x))')) 750 751 print clausify(lp.parse('some x.P(x)')) 752 print clausify(lp.parse('some x.all y.P(x,y)')) 753 print clausify(lp.parse('all y.some x.P(x,y)')) 754 print clausify(lp.parse('all z.all y.some x.P(x,y,z)')) 755 print clausify(lp.parse('all x.(all y.P(x,y) -> -all y.(Q(x,y) -> R(x,y)))'))

756 757 if __name__ == '__main__': 758 test_clausify() 759 print 760 testResolution() 761

Source Code for Module nltk.inference.resolution