Notes for November 7th, 2007

Discourse Representation Theory

DRS: <V, C>

C =
- P(t_1, ..., t_n)
- t_1 - t_2
- !Phi, Phi -> Psi, Phi or Psi

\vDash_{M, g} Phi: Condition Phi is tru in M under assignment g

h \vDash_{M, g} Phi: Assignmnment h is a verifying embedding for Phi
in M

Note: Here, Phi specifies <V, C> where all C are true and h and g are
the same except that they may differ on the variables in g (V).

\vDash_{M, g} Phi iff \exists h s.t. h \vDash_{M, g} Phi

\vDash_{M, g} P(t_1, ..., t_n) iff <||t||_{M, g},...,||t_n||_{M, g}>
in ||P||_m

\vDash_{M, g} !Phi iff there is no h s.t. h \vDash_{M, g} Phi includes
= 

\vDash_{M, g} Phi -> Psi iff for all h, if h \vDash_{M, g} Phi then
\exists k s.t. k \vDash{_M, h} Psi

\vDash_{M, g} Phi or Psi iff \exists h s.t. h \vDash_{M, g} Phi or h
\vDash_{M, g} Psi

h \vDash_{M, g} <{x_1, ..., x_n}, {Phi_1, ..., Phi_m}> iff
h[x_1,...,x_n]g and \vDash_{M, h} Phi_1, ..., \vDash_{M, h} Phi_m

Note: The notation h[x_1, ..., x_n]g indicates that h differs from g
only on the variables x_1, ..., x_n

Example 1:

John loves a girl that admires him. She loves him.

DRS:
V = {x, y}
C = {J=x, loves(y)(x), girl(y), admires(x)(y), loves(x)(y)}

Example 2:

Every farmer who owns a donkey beats it.

DRS:
V = {}
C = DRS_1 -> DRS_2

DRS_1:
V = {x, y}
C = {farmer(x), donkey(y), own(y)(x)}

DRS_2:
V = {}
C = {beats(y)(x)}

Example 3:

It is not the case that a man knows Mary. *He loves her.

DRS:
V = {y}
C = {!DRS_1, Mary = y, loves(y)(x)}

DRS_1:
V = {x}
C = {man(x), knows(y)(x)}

Example 4:

No man knows Mary. *He loves her.

DRS:
V = {y}
C = {DRS_1 -> !DRS_2, loves(y)(x), Mary = y}

DRS_1:
V = {x}
C = {man(x)}

DRS_2:
V = {}
C = {knows(y)(x)}

Examples (Problematic ones):

If a farmer owns a donkey, he beats it. ?He hates it.
- DRT predicts that this is fine

Every player chooses a pwn. He places it on the board.
- DRT predicts that this is wrong, but it's fine

Double negations

Either there is no washroom here or it is in a funny location
- Non classical uses of "or"

Mace
- Built at Argonne National Labs (~10 years ago)
- Now being largely replaced by Boolean Decision Diagrams
- A model builder
  - Put together with a theorem prover (e.g. OTTER)
  - Input Phi into both
    - Model builder tries to prove !Phi
    - Theorem prover tries to prove Phi

Phi_1 and Phi_2 and Phi_3

(1) FO fomrulae -> FO clauses
- Known as clausification

(2) FO clauses -> FO flat clauses
- known as flattening
  - n-ary functions -> n+1-ary predicates
  - P[t] -> P[x]|t != x
  - alpha = beta | L -> alpha != x|beta = x|L & alpha = x|beta !=
x|L (where alpha and beta are non-variables)
  - Rewrite function literals using n+1-ary predicates and new
variables
- f(g(x),x) = e
    !G(x,y) | !E(z) | F(y, x, z) & !G(x, y) | E(z) | !F(y, x, z)

(3) FO flat clause -> Propositional clause
- Propositionalizing
- Every m-ary relationa and a domain size = n
  => n^m expansion in search space
- Uniqueness constraints
  e.g. z_1 != z_2 | !F(x, y, z_1) | !F(x, y, z_2)
       F(x, y, 0) | ... | F(x, y, n-1)

(4) Propositional clause -> Propositional models
- Davis-Putnam Procedure (1960 - DP, 1962 - DPLL)
- Assumes we have CNF-SAT (c_1 & c_2 & ... & c_m) where each c_i = l_1
| l_2 | ... | l_k where l_j = x_k | !x_k

Three phases:

1) Unit propogation: Find all C_i s.t. k_i = 1
  - Eliminate c_i by setting l_1 = 1 and propogate
  - Iterate until we converge

2) Purity elimination
  - x_i is pure iff x_i only ever appears positively or only ever
appears negatively
  - then x_i must be set one way

3) Splitting rule

          Choose literal l_i
       /                      \ 
   l_i = 1                   l_i = 0
     /                          \
DPLL(c_1 & ... & c_m & l_i)  DPLL(c_1 & ... & c_m & !l_i)

- Basically brute force

Special predicate properties
  - Quasi-group
    - Multiplication table in Z(p)

  - Holey
    - Same as the quasi-groupo but there are holes in it

  - Bijection
    - Binary relation for a unary function

  - Equality

  - Order

  - Hole
    - Like bijecction but an injecetion and not a surjection