class_docstr: A first order model is a domain *D* of discourse and a valuation *V*.
  
  A domain *D* is a set, and a valuation *V* is a map that associates
  expressions with values in the model.
  The domain of *V* should be a subset of *D*.
  
  Construct a new ``Model``.
  
  :type domain: set
  :param domain: A set of entities representing the domain of discourse of the model.
  :type valuation: Valuation
  :param valuation: the valuation of the model.
  :param prop: If this is set, then we are building a propositional    model and don't require the domain of *V* to be subset of *D*.
class_docstr_tok: ["A","first","order","model","is","a","domain","*","D","*","of","discourse","and","a","valuation","*","V","*",".","A","domain","*","D","*","is","a","set",",","and","a","valuation","*","V","*","is","a","map","that","associates","expressions","with","values","in","the","model",".","The","domain","of","*","V","*","should","be","a","subset","of","*","D","*",".","Construct","a","new","``","Model","``",".",":","type","domain",":","set",":","param","domain",":","A","set","of","entities","representing","the","domain","of","discourse","of","the","model",".",":","type","valuation",":","Valuation",":","param","valuation",":","the","valuation","of","the","model",".",":","param","prop",":","If","this","is","set",",","then","we","are","building","a","propositional","model","and","do","n't","require","the","domain","of","*","V","*","to","be","subset","of","*","D","*","."]
docstr: Recursive interpretation function for a formula of first-order logic.
  
  Raises an ``Undefined`` error when ``parsed`` is an atomic string
  but is not a symbol or an individual variable.
  
  :return: Returns a truth value or ``Undefined`` if ``parsed`` is        complex, and calls the interpretation function ``i`` if ``parsed``        is atomic.
  
  :param parsed: An expression of ``logic``.
  :type g: Assignment
  :param g: an assignment to individual variables.
docstr_tok: ["Recursive","interpretation","function","for","a","formula","of","first-order","logic",".","Raises","an","``","Undefined","``","error","when","``","parsed","``","is","an","atomic","string","but","is","not","a","symbol","or","an","individual","variable",".",":","return",":","Returns","a","truth","value","or","``","Undefined","``","if","``","parsed","``","is","complex",",","and","calls","the","interpretation","function","``","i","``","if","``","parsed","``","is","atomic",".",":","param","parsed",":","An","expression","of","``","logic","``",".",":","type","g",":","Assignment",":","param","g",":","an","assignment","to","individual","variables","."]
code: def satisfy(self, parsed, g, trace=None):
      """
          Recursive interpretation function for a formula of first-order logic.
  
          Raises an ``Undefined`` error when ``parsed`` is an atomic string
          but is not a symbol or an individual variable.
  
          :return: Returns a truth value or ``Undefined`` if ``parsed`` is\
          complex, and calls the interpretation function ``i`` if ``parsed``\
          is atomic.
  
          :param parsed: An expression of ``logic``.
          :type g: Assignment
          :param g: an assignment to individual variables.
          """
  
      if isinstance(parsed, ApplicationExpression):
          function, arguments = parsed.uncurry()
          if isinstance(function, AbstractVariableExpression):
              # It's a predicate expression ("P(x,y)"), so used uncurried arguments
              funval = self.satisfy(function, g)
              argvals = tuple(self.satisfy(arg, g) for arg in arguments)
              return argvals in funval
          else:
              # It must be a lambda expression, so use curried form
              funval = self.satisfy(parsed.function, g)
              argval = self.satisfy(parsed.argument, g)
              return funval[argval]
      elif isinstance(parsed, NegatedExpression):
          return not self.satisfy(parsed.term, g)
      elif isinstance(parsed, AndExpression):
          return self.satisfy(parsed.first, g) and self.satisfy(
              parsed.second, g
          )
      elif isinstance(parsed, OrExpression):
          return self.satisfy(parsed.first, g) or self.satisfy(
              parsed.second, g
          )
      elif isinstance(parsed, ImpExpression):
          return (not self.satisfy(parsed.first, g)) or self.satisfy(
              parsed.second, g
          )
      elif isinstance(parsed, IffExpression):
          return self.satisfy(parsed.first, g) == self.satisfy(
              parsed.second, g
          )
      elif isinstance(parsed, EqualityExpression):
          return self.satisfy(parsed.first, g) == self.satisfy(
              parsed.second, g
          )
      elif isinstance(parsed, AllExpression):
          new_g = g.copy()
          for u in self.domain:
              new_g.add(parsed.variable.name, u)
              if not self.satisfy(parsed.term, new_g):
                  return False
          return True
      elif isinstance(parsed, ExistsExpression):
          new_g = g.copy()
          for u in self.domain:
              new_g.add(parsed.variable.name, u)
              if self.satisfy(parsed.term, new_g):
                  return True
          return False
      elif isinstance(parsed, IotaExpression):
          new_g = g.copy()
          for u in self.domain:
              new_g.add(parsed.variable.name, u)
              if self.satisfy(parsed.term, new_g):
                  return True
          return False
      elif isinstance(parsed, LambdaExpression):
          cf = {}
          var = parsed.variable.name
          for u in self.domain:
              val = self.satisfy(parsed.term, g.add(var, u))
              # NB the dict would be a lot smaller if we do this:
              # if val: cf[u] = val
              # But then need to deal with cases where f(a) should yield
              # a function rather than just False.
              cf[u] = val
          return cf
      else:
          return self.i(parsed, g, trace)
  
imports: import inspect
  import re
  import sys
  import textwrap
  from pprint import pformat
  from nltk.decorators import decorator
  from nltk.sem.logic import AbstractVariableExpression, AllExpression, AndExpression, ApplicationExpression, EqualityExpression, ExistsExpression, Expression, IffExpression, ImpExpression, IndividualVariableExpression, IotaExpression, LambdaExpression, NegatedExpression, OrExpression, Variable, is_indvar
label_desc: Use image node_id 5 for calling the Model obj's underlying member method code with example usage: obj.satisfy(parsed, g, trace) and returns: unknown, funval, unknown, unknown, unknown, unknown, unknown, unknown, True, False, False, False, True, cf, self, True