Package nltk_lite :: Package semantics :: Module evaluate
[hide private]
[frames] | no frames]

Source Code for Module nltk_lite.semantics.evaluate

  1  # Natural Language Toolkit: Models for first-order languages with lambda 
  2  # 
  3  # Copyright (C) 2001-2007 University of Pennsylvania 
  4  # Author: Ewan Klein <ewan@inf.ed.ac.uk>, 
  5  # URL: <http://nltk.sourceforge.net> 
  6  # For license information, see LICENSE.TXT 
  7  # 
  8  # $Id: evaluate.py 4206 2007-03-09 15:26:09Z ehk $ 
  9   
 10  """ 
 11  This module provides data structures for representing first-order 
 12  models.  
 13  """ 
 14   
 15  from nltk_lite.semantics import logic 
 16   
 17  from pprint import pformat 
 18   
19 -class Error(Exception): pass
20
21 -class Undefined(Error): pass
22
23 -class CharFun(dict):
24 """ 25 A dictionary which represents a curryed characteristic function. 26 """ 27
28 - def __init__(self, charfun=None):
29 dict.__init__(self) 30 if charfun: 31 #assert isinstance(charfun, dict) 32 self.update(charfun)
33 34
35 - def _isrel(self, s):
36 """Check whether a set represents a relation (of any arity).""" 37 38 assert isinstance(s, set), "Argument is not a set" 39 if len(s) == 0: 40 return True 41 elif not isinstance(max(s),tuple) or len(max(s))==len(min(s)): 42 return True 43 else: 44 raise ValueError, "Set contains sequences of different lengths"
45
46 - def _item2dict(self, item):
47 """ 48 Given an input such as the triple ('a', 'b', 'c'), return the L{CharFun} 49 {'c': {'b': {'a' : True}}} 50 51 @return: A characteristic function corresponding to the input. 52 @rtype: L{CharFun} 53 @param item: a literal or a tuple 54 """ 55 56 chf = {} 57 if isinstance(item, tuple): 58 # reverse the tuple 59 l = list(item) 60 l.reverse() 61 item = tuple(l) 62 if len(item)==1: 63 chf[item[0]] = True 64 elif len(item) > 1: 65 chf[item[0]] = self._item2dict(item[1:]) 66 else: 67 chf[item] = True 68 return chf
69
70 - def _merge(self, chf1, chf2):
71 k = chf2.keys()[0] 72 if k not in chf1: 73 chf1.update(chf2) 74 else: 75 self._merge(chf1[k], chf2[k]) 76 return chf1
77
78 - def read(self, s):
79 """ 80 Convert an M{n}-ary relation into its corresponding characteristic function. 81 @rtype: L{CharFun} 82 @type s: set 83 """ 84 85 assert isrel(s) 86 87 charfuns = [] 88 for item in s: 89 charfuns.append(self._item2dict(item)) 90 91 chf = reduce(self._merge, charfuns, {}) 92 self.update(chf)
93
94 - def tuples(self):
95 """ 96 Convert a L{CharFun} back into a set of tuples. 97 98 Given an input such as the L{CharFun} {'c': {'b': {'a': True}}}, 99 return set([('a', 'b', 'c')]) 100 """ 101 n = depth(self) 102 if n == 1: 103 tuples = self.domain 104 elif n == 2: 105 tuples = [(k2, k1) for k1 in self.keys() for k2 in self[k1].keys()] 106 elif n == 3: 107 tuples = [(k3, k2, k1) for k1 in self.keys() for k2 in self[k1].keys() for k3 in self[k1][k2].keys()] 108 else: 109 raise Error, "Only defined for CharFuns of depth <= 3" 110 result = set(tuples) 111 return result
112 113 ## def __repr__(self): 114 ## items = ['%s: %s' % t for t in sorted(self.items())] 115 ## return '{%s}' % ', '.join(items) 116
117 - def _getDomain(self):
118 return flatten(self)
119 120 domain = property(_getDomain, doc='Set-theoretic domain of a curried function')
121 122
123 -def isrel(s):
124 """ 125 Check whether a set represents a relation (of any arity). 126 127 @param s: a set containing tuples 128 @type s: set 129 """ 130 131 assert isinstance(s, set), "Argument is not a set" 132 if len(s) == 0: 133 return True 134 elif not isinstance(max(s),tuple) or len(max(s))==len(min(s)): 135 return True 136 else: 137 raise ValueError, "Set contains sequences of different lengths"
138
139 -def flatten(d):
140 """ 141 @return: The set of keys of a L{CharFun} instance. 142 @rtype: set 143 @type d: dict 144 """ 145 flat = [] 146 try: 147 flat.extend(d.keys()) 148 for v in d.values(): 149 if isinstance(v, dict): 150 flat.extend(flatten(v)) 151 else: 152 flat.append(v) 153 except AttributeError: 154 flat.append(d) 155 result = set(flat) 156 result.discard(True) 157 return result
158 159
160 -def depth(cf):
161 """ 162 Calculate the depth of a L{CharFun}. 163 164 @rtype: C{int} 165 @type cf: L{CharFun} 166 """ 167 if True in cf.values(): 168 return 1 169 else: 170 key = cf.keys()[0] 171 return 1+depth(cf[key])
172 173
174 -class Valuation(dict):
175 """ 176 A dictionary which represents a model-theoretic Valuation of non-logical constants. 177 178 179 An attempt to initialize a L{Valuation} with an individual 180 variable expression (e.g., 'x3') will raise an error, as will an 181 attemp to read a list containing an individual variable 182 expression. 183 184 An instance of L{Valuation} will raise a KeyError exception (i.e., 185 just behave like a standard dictionary) if indexed with an expression that 186 is not in its list of symbols. 187 """
188 - def __init__(self, valuation=None):
189 dict.__init__(self) 190 if valuation: 191 for k in valuation.keys(): 192 if logic.is_indvar(k): 193 raise Error, "This looks like an individual variable: '%s'" % k 194 # Check if the valuation is of the form {'p': True} 195 if isinstance(valuation[k], bool): 196 self[k] = valuation[k] 197 else: 198 try: 199 cf = CharFun(valuation[k]) 200 self[k] = cf 201 except (TypeError, ValueError): 202 self[k] = valuation[k]
203
204 - def __getitem__(self, key):
205 if key in self: 206 return dict.__getitem__(self, key) 207 else: 208 raise Undefined, "Unknown expression: '%s'" % key
209
210 - def read(self, seq):
211 """ 212 Parse a list such as C{[('j', 'b1'), ('girl', set(['g1', 'g2']))]} into a L{Valuation}. 213 @rtype: L{Valuation} 214 @param seq: A list of tuples of the form (I{constant}, I{relation}), where I{relation} is a set of tuples. 215 """ 216 d = dict(seq) 217 for k in d.keys(): 218 if logic.is_indvar(k): 219 raise Error, "This looks like an individual variable: '%s'" % k 220 val = d[k] 221 if isinstance(val, str): 222 pass 223 else: 224 cf = CharFun() 225 cf.read(d[k]) 226 d[k] = cf 227 self.update(d)
228
229 - def __str__(self):
230 return pformat(self)
231
232 - def _getDomain(self):
233 dom = set() 234 for v in self.values(): 235 flat = flatten(v) 236 dom = dom.union(flat) 237 return dom
238 239 domain = property(_getDomain, 240 doc='Set-theoretic domain of the value-space of a Valuation.') 241
242 - def _getSymbols(self):
243 return self.keys()
244 245 symbols = property(_getSymbols, 246 doc='The non-logical constants which the Valuation recognizes.')
247 248
249 -class Assignment(dict):
250 """ 251 A dictionary which represents an assignment of values to variables. 252 253 An assigment can only assign values from its domain. 254 255 If an unknown expression M{a} is passed to a model M{M}'s 256 interpretation function M{i}, M{i} will first check whether M{M}'s 257 valuation assigns an interpretation to M{a} as a constant, and if 258 this fails, M{i} will delegate the interpretation of M{a} to 259 M{g}. M{g} only assigns values to individual variables (i.e., 260 members of the class L{IndVariableExpression} in the L{logic} 261 module. If a variable is not assigned a value by M{g}, it will raise 262 an C{Undefined} exception. 263 """
264 - def __init__(self, domain, assignment=None):
265 dict.__init__(self) 266 self.domain = domain 267 if assignment: 268 for var in assignment.keys(): 269 val = assignment[var] 270 assert val in self.domain,\ 271 "'%s' is not in the domain: %s" % (val, self.domain) 272 assert logic.is_indvar(var),\ 273 "Wrong format for an Individual Variable: '%s'" % var 274 self.update(assignment) 275 self._addvariant()
276
277 - def __getitem__(self, key):
278 if key in self: 279 return dict.__getitem__(self, key) 280 else: 281 raise Undefined, "Not recognized as a variable: '%s'" % key
282
283 - def copy(self):
284 new = Assignment(self.domain) 285 new.update(self) 286 return new
287
288 - def purge(self, var=None):
289 """ 290 Remove one or all keys (i.e. logic variables) from an 291 assignment, and update C{self.variant}. 292 293 @param var: a Variable acting as a key for the assignment. 294 """ 295 if var: 296 val = self[var] 297 del self[var] 298 else: 299 self.clear() 300 self._addvariant() 301 return None
302
303 - def __str__(self):
304 """ 305 Pretty printing for assignments. {'x', 'u'} appears as 'g[u/x]' 306 """ 307 gstring = "g" 308 for (val, var) in self.variant: 309 gstring = gstring + "[" + str(val) + "/" + str(var) + "]" 310 return gstring
311
312 - def _addvariant(self):
313 """ 314 Create a more pretty-printable version of the assignment. 315 """ 316 list = [] 317 for item in self.items(): 318 pair = (item[1], item[0]) 319 list.append(pair) 320 self.variant = list 321 return None
322
323 - def add(self, val, var):
324 """ 325 Add a new variable-value pair to the assignment, and update 326 C{self.variant}. 327 328 We write the arguments in the order 'val, var' by analogy with the 329 notation 'g[u/x]'. 330 """ 331 assert val in self.domain,\ 332 "%s is not in the domain %s" % (val, self.domain) 333 assert logic.is_indvar(var),\ 334 "Wrong format for an Individual Variable: '%s'" % var 335 self[var] = val 336 self._addvariant() 337 return self
338 339
340 -class Model:
341 """ 342 A first order model is a domain M{D} of discourse and a valuation M{V}. 343 344 A domain M{D} is a set, and a valuation M{V} is a map that associates 345 expressions with values in the model. 346 The domain of M{V} should be a subset of M{D}. 347 348 349 """ 350
351 - def __init__(self, domain, valuation, prop=None):
352 """ 353 Construct a new L{Model}. 354 355 @type domain: C{set} 356 @param domain: A set of entities representing the domain of discourse of the model. 357 @type valuation: L{Valuation} 358 @param valuation: the valuation of the model. 359 @param prop: If this is set, then we are building a propositional\ 360 model and don't require the domain of M{V} to be subset of M{D}. 361 """ 362 assert isinstance(domain, set) 363 self.domain = domain 364 self.valuation = valuation 365 if prop is None: 366 if not domain.issuperset(valuation.domain): 367 raise Error,\ 368 "The valuation domain, %s, must be a subset of the model's domain, %s"\ 369 % (valuation.domain, domain)
370 371
372 - def __repr__(self):
373 return "(%r, %r)" % (self.domain, self.valuation)
374
375 - def __str__(self):
376 return "Domain = %s,\nValuation = \n%s" % (self.domain, self.valuation)
377
378 - def app(self, fun, arg):
379 """ 380 Wrapper for handling KeyErrors and TypeErrors raised by 381 function application. 382 383 This constrains instances of L{CharFun} to return C{False} in 384 the right circumstances. 385 386 @param fun: an instance of L{CharFun}. 387 @param arg: an arbitrary semantic object 388 @return: If C{arg} is in C{fun}'s domain, then returns C{fun[arg]},\ 389 else if C{arg} is in C{self.domain}, returns C{False},\ 390 else raises C{Undefined} error. 391 """ 392 393 try: 394 return fun[arg] 395 except KeyError: 396 if arg in self.domain: 397 return False 398 else: 399 raise Undefined,\ 400 "%s can't be applied as a function to '%s'" % (fun, arg) 401 except TypeError: 402 if fun == False: 403 return False 404 else: 405 raise Undefined,\ 406 "%s can't be applied as a function to %s" % (fun, arg)
407 408 409 410 NOT = {True: False, False: True} 411 AND = {True: {True: True, False: False}, 412 False: {True: False, False: False}} 413 OR = {True: {True: True, False: True}, 414 False: {True: True, False: False}} 415 IMPLIES = {True: {True: True, False: False}, 416 False: {True: True, False: True}} 417 IFF = {True: {True: True, False: False}, 418 False: {True: False, False: True}} 419 420 OPS = {'and': AND, 421 'or': OR, 422 'implies': IMPLIES, 423 'iff': IFF} 424
425 - def evaluate(self, expr, g, trace=None):
426 """ 427 Provides a handler for L{satisfy} 428 that blocks further propagation of C{Undefined} error. 429 @param expr: An C{Expression} of L{logic}. 430 @type g: L{Assignment} 431 @param g: an assignment to individual variables. 432 @rtype: C{bool} or 'Undefined' 433 """ 434 try: 435 value = self.satisfy(expr, g, trace=trace) 436 if trace: 437 print "'%s' evaluates to %s under M, %s" % (expr, value, g) 438 return value 439 except Undefined: 440 return 'Undefined'
441 442 443
444 - def satisfy(self, expr, g, trace=None):
445 """ 446 Recursive interpretation function for a formula of first-order logic. 447 448 Raises an C{Undefined} error when C{expr} is an atomic string 449 but is not a symbol or an individual variable. 450 451 @return: Returns a truth value or C{Undefined} if C{expr} is\ 452 complex, and calls the interpretation function C{i} if C{expr}\ 453 is atomic. 454 455 @param expr: An expression of L{logic}. 456 @type g: L{Assignment} 457 @param g: an assignment to individual variables. 458 """ 459 460 OPS = Model.OPS 461 462 # OPS = {'and': Model.AND, 463 # 'or': Model.OR, 464 # 'implies': Model.IMPLIES, 465 # 'iff': Model.IFF} 466 467 468 try: 469 parsed = self.decompose(expr) 470 # expr is a variable or constant; we don't want to decompose it further 471 if isinstance(parsed, str): 472 return self.i(expr, g, trace) 473 # parsed is a pair of strings 474 else: 475 first, second = parsed 476 # maybe _first_ is an operator like 'and', 'not' or '=' and _second_ is a list of args 477 phi = second[0] 478 try: 479 psi = second[1] 480 # second can't be decomposed further 481 except IndexError: 482 pass 483 484 if first == 'not': 485 if trace: 486 print " '%s' evaluates to %s under M, %s." % (phi, self.satisfy(phi, g), g) 487 return not self.satisfy(phi, g, trace) 488 489 elif first in OPS: 490 value = OPS[first][self.satisfy(phi, g, trace)][self.satisfy(psi, g, trace)] 491 if trace: 492 print " '%s' evaluates to %s under M, %s" % (phi, self.satisfy(phi, g, trace), g) 493 print " '%s' evaluates to %s under M, %s" % (psi, self.satisfy(psi, g, trace), g) 494 return value 495 496 elif first == '=': 497 value = (self.satisfy(phi, g, trace) == self.satisfy(psi, g, trace)) 498 if trace: 499 print " '%s' evaluates to %s under M, %s" % (phi, self.satisfy(phi, g, trace), g) 500 print " '%s' evaluates to %s under M, %s" % (psi, self.satisfy(psi, g, trace), g) 501 return value 502 503 504 # _first_ is something like '\\ x' and _second_ is something like '(boy x)' 505 elif first[0] == '\\': 506 var = first[1] 507 phi = second 508 cf = CharFun() 509 for u in self.domain: 510 val = self.satisfy(phi, g.add(u, var), trace) 511 if val: 512 cf[u] = val 513 514 if trace: 515 print " '%s' evaluates to %s under M, %s" % (expr, cf, g) 516 return cf 517 518 # _first_ is something like 'some x' and _second_ is something like '(boy x)' 519 elif first[0] == 'some': 520 var = first[1] 521 phi = second 522 # seq is an iterator 523 seq = self.satisfiers(phi, var, g, trace, nesting=1) 524 #any returns True if seq is nonempty 525 value = self.any(seq) 526 if trace: 527 if value: 528 print " '%s' evaluates to %s under M, %s" % (phi, value, g) 529 if trace > 1: 530 print " satisfiers of %s under %s are %s" % (phi, g, sat) 531 else: 532 print " '%s' evaluates to %s under M, %s" % (phi, value, g) 533 if trace > 1: 534 print " satisfiers of %s under %s are %s" % (phi, g, sat) 535 return value 536 537 elif first[0] == 'all': 538 var = first[1] 539 phi = second 540 sat = self.satisfiers(phi, var, g, trace, nesting=1) 541 #issubset can take an iterator as argument 542 value = self.domain.issubset(sat) 543 if trace: 544 if value: 545 print " '%s' evaluates to %s under M, %s" % (phi, self.satisfy(phi, g, trace), g) 546 else: 547 notphi = '(not %s)' % phi 548 witness = self.satisfiers(notphi, var, g).pop() 549 g.add(witness, var) 550 print " '%s' evaluates to %s under M, %s" % (phi, self.satisfy(phi, g, trace), g) 551 552 return value 553 554 # maybe _first_ is something like 'boy' and _second_ is an argument expression like 'x' 555 else: 556 try: 557 funval = self.satisfy(first, g, trace) 558 argval = self.satisfy(second, g, trace) 559 app = self.app(funval, argval) 560 if trace > 1: 561 print "'%s': %s applied to %s yields %s"\ 562 % (expr, funval, argval, app) 563 return app 564 # we can't get a proper interpretation 565 except TypeError: 566 print "The interpretation of %s cannot be applied to the interpretation of %s"\ 567 % (first, second) 568 print "'%s': %s applied to %s yields %s"\ 569 % (expr, funval, argval, app) 570 raise 571 572 except ValueError: 573 raise Undefined, "Cannot parse %s", expr
574 575 576
577 - def i(self, expr, g, trace=False):
578 """ 579 An interpretation function. 580 581 Assuming that C{expr} is atomic: 582 583 - if C{expr} is a non-logical constant, calls the valuation M{V} 584 - else if C{expr} is an individual variable, calls assignment M{g} 585 - else returns C{Undefined}. 586 587 588 @param expr: an C{Expression} of L{logic}. 589 @type g: L{Assignment} 590 @param g: an assignment to individual variables. 591 @return: a semantic value 592 """ 593 try: 594 if trace > 1: 595 print " i, %s('%s') = %s" % (g, expr, self.valuation[expr]) 596 # expr is a non-logical constant, i.e., in self.valuation.symbols 597 return self.valuation[expr] 598 except Undefined: 599 if trace > 1: 600 print " (checking whether '%s' is an individual variable)" % expr 601 602 # expr wasn't a constant; maybe a variable that g knows about? 603 return g[expr]
604 605 606
607 - def freevar(self, var, expr):
608 """ 609 Is C{var} one of the free variables in C{expr}? 610 611 @type var: an C{Indvar} of L{logic} 612 @param var: the variable to test for. 613 @param expr: an C{Expression} of L{logic}. 614 @rtype: C{bool} 615 """ 616 parsed = logic.Parser().parse(expr) 617 variable = logic.Variable(var) 618 return variable in parsed.free()
619
620 - def satisfiers(self, expr, var, g, trace=False, nesting=0):
621 """ 622 Generate the entities from the model's domain that satisfy an open formula. 623 624 @param expr: the open formula 625 @param var: the relevant free variable in C{expr}. 626 @param g: the variable assignment 627 @return: an iterator over the entities that satisfy C{expr}. 628 """ 629 630 spacer = ' ' 631 indent = spacer + (spacer * nesting) 632 candidates = [] 633 634 if self.freevar(var, expr): 635 if trace: 636 print 637 print (spacer * nesting) + "Open formula is '%s' with assignment %s" % (expr, g) 638 for u in self.domain: 639 new_g = g.copy() 640 new_g.add(u, var) 641 if trace > 1: 642 lowtrace = trace-1 643 else: 644 lowtrace = 0 645 value = self.satisfy(expr, new_g, lowtrace) 646 647 if trace: 648 print indent + "(trying assignment %s)" % new_g 649 650 # expr == False under g[u/var]? 651 if value == False: 652 if trace: 653 print indent + "value of '%s' under %s is False" % (expr, new_g) 654 655 656 # so g[u/var] is a satisfying assignment 657 else: 658 candidates.append(u) 659 if trace: 660 print indent + "value of '%s' under %s is %s" % (expr, new_g, value) 661 662 result = (c for c in candidates) 663 # var isn't free in expr 664 else: 665 raise Undefined, "%s is not free in %s" % (var, expr) 666 667 return result
668 669
670 - def decompose(self, expr):
671 """ 672 Function to communicate with a first-order functional language. 673 674 This function tries to make weak assumptions about the parse structure 675 provided by the logic module. It makes the assumption that an expression 676 can be broken down into a pair of subexpressions: 677 678 - The C{(binder, body)} pair is for decomposing quantified formulae. 679 - The C{(op, args)} pair is for decomposing formulae with a boolean operator. 680 - The C{(fun, args)} pair should catch other relevant cases. 681 682 @param expr: A string representation of a first-order formula. 683 """ 684 685 try: 686 parsed = logic.Parser(constants=self.valuation.symbols).parse(expr) 687 except TypeError: 688 print "Cannot parse %s" % expr 689 690 try: 691 first, second = parsed.binder, parsed.body 692 #print 'first is %s, second is %s' % (first, second) 693 return (first, second) 694 except AttributeError: 695 pass 696 try: 697 first, second = parsed.op, parsed.args 698 #print 'first is %s, second is %s' % (first, second) 699 return (first, second) 700 except AttributeError: 701 pass 702 try: 703 first, second = str(parsed.first), str(parsed.second) 704 #print 'first is %s, second is %s' % (first, second) 705 return (first, second) 706 except (AttributeError, TypeError): 707 return expr
708
709 - def any(self, seq):
710 """ 711 Returns True if there is at least one element in the iterable. 712 713 @param seq: an iterator 714 @rtype: C{bool} 715 """ 716 for elem in seq: 717 return True 718 return False
719 720 721 722 #////////////////////////////////////////////////////////////////////// 723 # Demo.. 724 #////////////////////////////////////////////////////////////////////// 725 # number of spacer chars 726 mult = 30 727
728 -def propdemo(trace=None):
729 """Example of a propositional model.""" 730 731 global val1, dom1, m1, g1 732 val1 = Valuation({'p': True, 'q': True, 'r': False}) 733 dom1 = set([]) 734 m1 = Model(dom1, val1, prop=True) 735 g1 = Assignment(dom1) 736 737 print 738 print '*' * mult 739 print "Propositional Formulas Demo" 740 print '*' * mult 741 print "Model m1:\n", m1 742 print '*' * mult 743 744 sentences = [ 745 '(p and q)', 746 '(p and r)', 747 '(not p)', 748 '(not r)', 749 '(not (not p))', 750 '(not (p and r))', 751 '(p or r)', 752 '(r or p)', 753 '(r or r)', 754 '((not p) or r))', 755 '(p or (not p))', 756 '(p implies q)', 757 '(p implies r)', 758 '(r implies p)', 759 '(p iff p)', 760 '(r iff r)', 761 '(p iff r)', 762 ] 763 764 for sent in sentences: 765 if trace: 766 print 767 m1.evaluate(sent, g1, trace) 768 else: 769 print "The value of '%s' is: %s" % (sent, m1.evaluate(sent, g1))
770
771 -def folmodel(trace=None):
772 """Example of a first-order model.""" 773 774 global val2, v2, dom2, m2, g2 775 val2 = Valuation() 776 v2 = [('adam', 'b1'), ('betty', 'g1'), ('fido', 'd1'),\ 777 ('girl', set(['g1', 'g2'])), ('boy', set(['b1', 'b2'])), ('dog', set(['d1'])), 778 ('love', set([('b1', 'g1'), ('b2', 'g2'), ('g1', 'b1'), ('g2', 'b1')]))] 779 val2.read(v2) 780 dom2 = val2.domain 781 m2 = Model(dom2, val2) 782 g2 = Assignment(dom2, {'x': 'b1', 'y': 'g2'}) 783 784 if trace: 785 print "*" * mult 786 print "Model m2\n", m2 787 print "*" * mult 788 789 symbols = ['adam', 'girl', 'love', 'walks', 'x', 'y', 'z'] 790 791 if trace: 792 for s in symbols: 793 try: 794 print "The interpretation of '%s' in m2 is %s" % (s, m2.i(s, g2)) 795 except Undefined: 796 print "The interpretation of '%s' in m2 is Undefined" % s
797
798 -def foldemo(trace=None):
799 """Interpretation of closed expressions in a first-order model.""" 800 folmodel() 801 802 print 803 print '*' * mult 804 print "FOL Formulas Demo" 805 print '*' * mult 806 807 formulas = [ 808 '(love adam betty)', 809 '(adam = mia)', 810 '\\x. ((boy x) or (girl x))', 811 '\\x y. ((boy x) and (love y x))', 812 '\\x. some y. ((boy x) and (love y x))', 813 'some z1. (boy z1)', 814 'some x. ((boy x) and (not (x = adam)))', 815 'some x. ((boy x) and all y. (love x y))', 816 'all x. ((boy x) or (girl x))', 817 'all x. ((girl x) implies some y. (boy y) and (love y x))', #Every girl loves some boy. 818 'some x. ((boy x) and all y. ((girl y) implies (love x y)))', #There is some boy that every girl loves. 819 'some x. ((boy x) and all y. ((girl y) implies (love y x)))', #Some boy loves every girl. 820 'all x. ((dog x) implies (not (girl x)))', 821 'some x. some y. ((love y x) and (love y x))' 822 ] 823 824 825 for fmla in formulas: 826 g2.purge() 827 if trace: 828 print 829 m2.evaluate(fmla, g2, trace) 830 else: 831 print "The value of '%s' is: %s" % (fmla, m2.evaluate(fmla, g2))
832 833
834 -def satdemo(trace=None):
835 """Satisfiers of an open formula in a first order model.""" 836 837 print 838 print '*' * mult 839 print "Satisfiers Demo" 840 print '*' * mult 841 842 folmodel() 843 844 formulas = [ 845 '(boy x)', 846 '(x = x)', 847 '((boy x) or (girl x))', 848 '((boy x) and (girl x))', 849 '(love x adam)', 850 '(love adam x)', 851 '(not (x = adam))', 852 'some z22. (love z22 x)', 853 'some y. (love x y)', 854 'all y. ((girl y) implies (love y x))', 855 'all y. ((girl y) implies (love x y))', 856 'all y. ((girl y) implies ((boy x) and (love x y)))', 857 '((boy x) and all y. ((girl y) implies (love y x)))', 858 '((boy x) and all y. ((girl y) implies (love x y)))', 859 '((boy x) and some y. ((girl y) and (love x y)))', 860 '((girl x) implies (dog x))', 861 'all y. ((dog y) implies (x = y))', 862 '(not some y. (love x y))', 863 'some y. ((love y adam) and (love x y))' 864 ] 865 866 if trace: 867 print m2 868 869 for fmla in formulas: 870 g2.purge() 871 print "The satisfiers of '%s' are: %s" % (fmla, list(m2.satisfiers(fmla, 'x', g2, trace)))
872 873
874 -def demo(num, trace=None):
875 """ 876 Run some demos. 877 878 - num = 1: propositional logic demo 879 - num = 2: first order model demo (only if trace is set) 880 - num = 3: first order sentences demo 881 - num = 4: satisfaction of open formulas demo 882 - any other value: run all the demos 883 884 @param trace: trace = 1, or trace = 2 for more verbose tracing 885 """ 886 demos = {1: propdemo, 887 2: folmodel, 888 3: foldemo, 889 4: satdemo} 890 891 892 try: 893 demos[num](trace=trace) 894 except KeyError: 895 for num in demos.keys(): 896 demos[num](trace=trace)
897 898 899 900 if __name__ == "__main__": 901 demo(5, trace=0) 902