Representing Kripke Interpretations

Using the (new) TPTP format for Tarskian Interpretations

Kripke Worlds

• New defined type $ki_world
• New defined constant $ki_local_world
• New defined predicates $ki_accessible, $ki_world_is
• Specify worlds

  ( ! [W: $ki_world] : ( W = w1 | W = w2 )
  & $distinct(w1,w2)
  & $ki_local_world = w1
  & $ki_accessible(w1,w1)     %----Logic is M
  & $ki_accessible(w2,w2)
  & $ki_accessible(w1,w2) ) 

• Tarskian interpretation for each world

  ( $ki_world_is(w1,
    ( ( ! [P: person] : ? [DP: d_person] : P = d2person(DP)
      & ! [DP: d_person] : ( DP = d_alex | DP = d_chris )
      & $distinct(d_alex,d_chris)
      & ? [DP: d_person] : ( DP = d_alex )
      & ? [DP: d_person] : ( DP = d_chris )
      & ! [DP1: d_person,DP2: d_person] : 
          ( d2person(DP1) = d2person(DP2) => DP1 = DP2 )
      & ! [P: product] : ? [DP: d_product] : P = d2product(DP)
      & ! [DP: d_product] : DP = d_leo
      & ? [DP: d_product] : DP = d_leo
      & ! [DP1: d_product,DP2: d_product] :
          ( d2product(DP1) = d2product(DP2) => DP1 = DP2 ) )
    & ( alex = d2person(d_alex)
      & chris = d2person(d_chris)
      & leo = d2product(d_leo) )
    & ( work_hard(d2person(d_alex),d2product(d_leo))
      & work_hard(d2person(d_chris),d2product(d_leo))
      & ~ gets_rich(d2person(d_alex))
      & gets_rich(d2person(d_chris)) ) ) ) ) 

Examples

• Work to get Someone Rich has this model