\documentclass{article}
\usepackage{fleqn}
\usepackage{epsf}
\usepackage[dvips]{color}
\usepackage{aima2e-slides}


\begin{document}

\begin{huge}
\titleslide{Inference in first-order logic}{Chapter 9}

\sf

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Outline}

\blob Reducing first-order inference to propositional inference

\blob Unification

\blob Generalized Modus Ponens

\blob Forward and backward chaining

\blob Logic programming

\blob Resolution

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{A brief history of reasoning}

\begin{tabular}{lll}
\note{450{\sc b.c.}} &\txr{ Stoics      }& propositional logic, inference (maybe) \\
\note{322{\sc b.c.} }&\txr{ Aristotle   }& ``syllogisms'' (inference rules), quantifiers \\
\note{1565 }&\txr{ Cardano     }& probability theory (propositional logic + uncertainty) \\
\note{1847 }&\txr{ Boole       }& propositional logic (again) \\
\note{1879 }&\txr{ Frege       }& first-order logic \\
\note{1922 }&\txr{ Wittgenstein}& proof by truth tables \\
\note{1930 }&\txr{ G\"odel     }& $\exists$ complete algorithm for FOL \\
\note{1930 }&\txr{ Herbrand    }& complete algorithm for FOL (reduce to propositional) \\
\note{1931 }&\txr{ G\"odel     }& $\lnot\exists$ complete algorithm for arithmetic \\
\note{1960 }&\txr{ Davis/Putnam}& ``practical'' algorithm for propositional logic \\
\note{1965 }&\txr{ Robinson    }& ``practical'' algorithm for FOL---resolution
\end{tabular}


%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Universal instantiation (UI)}

Every instantiation of a universally quantified sentence is entailed by it:
\mat{\[\frac{\All{v} \alpha}{\noprog{Subst}(\{v/g\},\alpha)}\]}
for any variable \mat{$v$} and ground term \mat{$g$}

E.g., \mat{$\All{x} King(x) \land Greedy(x) \implies Evil(x)$} yields
\mat{\begin{formula}
   King(John) \land Greedy(John)  \implies Evil(John)\\
   King(Richard) \land Greedy(Richard)  \implies Evil(Richard)\\
   King(Father(John)) \land Greedy(Father(John))  \implies Evil(Father(John))\\
   \quad\vdots
\end{formula}}



%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Existential instantiation (EI)}

For any sentence \mat{$\alpha$}, variable \mat{$v$}, and constant symbol \mat{$k$}\\
\emph{that does not appear elsewhere in the knowledge base}:
\mat{\[\frac{\Exi{v} \alpha}{\noprog{Subst}(\{v/k\},\alpha)}\]}

E.g., \mat{$\Exi{x} Crown(x) \land OnHead(x,John)$} yields
\mat{\[
Crown(C_1) \land OnHead(C_1,John)
\]}
provided \mat{$C_1$} is a new constant symbol, called a \defn{Skolem constant}

Another example: from \mat{$\Exi{x} {{d(x^y)}/{dy}} \eq  x^y$} we obtain
\mat{\[
{{d(e^y)}/{dy}} \eq  e^y
\]}
provided \mat{$e$} is a new constant symbol

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Existential instantiation contd.}

UI can be applied several times to \emph{add} new sentences;\\
the new KB is logically equivalent to the old

EI can be applied once to \emph{replace} the existential sentence;\\
the new KB is \emph{not} equivalent to the old,\\
but is satisfiable iff the old KB was satisfiable

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Reduction to propositional inference}

Suppose the KB contains just the following:
\mat{\begin{formula}
   \All{x} King(x) \land Greedy(x) \implies Evil(x)\\
   King(John)\\
   Greedy(John)\\
   Brother(Richard,John)
\end{formula}}
Instantiating the universal sentence in \emph{all possible} ways, we have
\mat{\begin{formula}
   King(John) \land Greedy(John) \implies Evil(John)\\
   King(Richard) \land Greedy(Richard) \implies Evil(Richard)\\
   King(John)\\
   Greedy(John)\\
   Brother(Richard,John)
\end{formula}}
The new KB is \defn{propositionalized}: proposition symbols are
\mat{\[
  King(John),\ Greedy(John),\ Evil(John), King(Richard)\, \bbox{etc.}
\]}

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Reduction contd.}

Claim: a ground sentence\mat{$^*$} is entailed by new KB iff entailed by original KB

Claim: every FOL KB can be propositionalized so as to preserve entailment

Idea: propositionalize KB and query, apply resolution, return result

Problem: with function symbols, there are infinitely many ground terms,\al
  e.g., \mat{$Father(Father(Father(John)))$}

Theorem: Herbrand (1930). If a sentence \mat{$\alpha$} is entailed by an FOL KB,\nl
  it is entailed by a \emph{finite} subset of the propositional KB

Idea: For \mat{$n$} = \mat{$0$} to \mat{$\infty$} do\nl
    create a propositional KB by instantiating with depth-\mat{$n$} terms\nl
    see if \mat{$\alpha$} is entailed by this KB

Problem: works if \mat{$\alpha$} is entailed, loops if \mat{$\alpha$} is not entailed

Theorem: Turing (1936), Church (1936), entailment in FOL is \defn{semidecidable}


%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Problems with propositionalization}

Propositionalization seems to generate lots of irrelevant sentences.\\
E.g., from 
\mat{\begin{formula}
   \All{x} King(x) \land Greedy(x) \implies Evil(x)\\
   King(John)\\
   \All{y} Greedy(y)\\
   Brother(Richard,John)
\end{formula}}
it seems obvious that \mat{$Evil(John)$}, but propositionalization produces
lots of facts such as \mat{$Greedy(Richard)$} that are irrelevant

With \mat{$p$} \mat{$k$}-ary predicates and \mat{$n$} constants, there are \mat{$p\cdot n^k$} instantiations

With function symbols, it gets nuch much worse!



%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Unification}

We can get the inference immediately if we can find a substitution \mat{$\theta$}\\
such that \mat{$King(x)$} and \mat{$Greedy(x)$} match \mat{$King(John)$} and \mat{$Greedy(y)$}

\mat{$\theta = \{x/John,y/John\}$} works

\mat{\noprog{Unify}}\mat{$(\alpha,\beta) = \theta$} if \mat{$\alpha\theta\eq \beta\theta$}

\mat{\[\begin{array}{l|l|l}
p & q & \theta \\
\hline
Knows(John,x) & Knows(John,Jane) & \\
Knows(John,x) & Knows(y,OJ)      & \\
Knows(John,x) & Knows(y,Mother(y))& \phantom{\{y/John,x/Mother(John)\}}\\
Knows(John,x) & Knows(x,OJ)
\end{array}\]}

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Unification}

We can get the inference immediately if we can find a substitution \mat{$\theta$}\\
such that \mat{$King(x)$} and \mat{$Greedy(x)$} match \mat{$King(John)$} and \mat{$Greedy(y)$}

\mat{$\theta = \{x/John,y/John\}$} works

\mat{\noprog{Unify}}\mat{$(\alpha,\beta) = \theta$} if \mat{$\alpha\theta\eq \beta\theta$}

\mat{\[\begin{array}{l|l|l}
p & q & \theta \\
\hline
Knows(John,x) & Knows(John,Jane) & \hbox{\note{$\{x/Jane\}$}}\\
Knows(John,x) & Knows(y,OJ)      & \\
Knows(John,x) & Knows(y,Mother(y))& \phantom{\{y/John,x/Mother(John)\}}\\
Knows(John,x) & Knows(x,OJ)
\end{array}\]}

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Unification}

We can get the inference immediately if we can find a substitution \mat{$\theta$}\\
such that \mat{$King(x)$} and \mat{$Greedy(x)$} match \mat{$King(John)$} and \mat{$Greedy(y)$}

\mat{$\theta = \{x/John,y/John\}$} works

\mat{\noprog{Unify}}\mat{$(\alpha,\beta) = \theta$} if \mat{$\alpha\theta\eq \beta\theta$}

\mat{\[\begin{array}{l|l|l}
p & q & \theta \\
\hline
Knows(John,x) & Knows(John,Jane) & \hbox{\note{$\{x/Jane\}$}}\\
Knows(John,x) & Knows(y,OJ)      & \hbox{\note{$\{x/OJ,y/John\}$}}\\
Knows(John,x) & Knows(y,Mother(y))& \phantom{\{y/John,x/Mother(John)\}}\\
Knows(John,x) & Knows(x,OJ)
\end{array}\]}

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Unification}

We can get the inference immediately if we can find a substitution \mat{$\theta$}\\
such that \mat{$King(x)$} and \mat{$Greedy(x)$} match \mat{$King(John)$} and \mat{$Greedy(y)$}

\mat{$\theta = \{x/John,y/John\}$} works

\mat{\noprog{Unify}}\mat{$(\alpha,\beta) = \theta$} if \mat{$\alpha\theta\eq \beta\theta$}

\mat{\[\begin{array}{l|l|l}
p & q & \theta \\
\hline
Knows(John,x) & Knows(John,Jane) & \hbox{\note{$\{x/Jane\}$}}\\
Knows(John,x) & Knows(y,OJ)      & \hbox{\note{$\{x/OJ,y/John\}$}}\\
Knows(John,x) & Knows(y,Mother(y))& \hbox{\note{$\{y/John,x/Mother(John)\}$}}\\
Knows(John,x) & Knows(x,OJ)
\end{array}\]}


%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Unification}

We can get the inference immediately if we can find a substitution \mat{$\theta$}\\
such that \mat{$King(x)$} and \mat{$Greedy(x)$} match \mat{$King(John)$} and \mat{$Greedy(y)$}

\mat{$\theta = \{x/John,y/John\}$} works

\mat{\noprog{Unify}}\mat{$(\alpha,\beta) = \theta$} if \mat{$\alpha\theta\eq \beta\theta$}

\mat{\[\begin{array}{l|l|l}
p & q & \theta \\
\hline
Knows(John,x) & Knows(John,Jane) & \hbox{\note{$\{x/Jane\}$}}\\
Knows(John,x) & Knows(y,OJ)      & \hbox{\note{$\{x/OJ,y/John\}$}}\\
Knows(John,x) & Knows(y,Mother(y))& \hbox{\note{$\{y/John,x/Mother(John)\}$}}\\
Knows(John,x) & Knows(x,OJ) & \hbox{\note{$fail$}}
\end{array}\]}
\defn{Standardizing apart} eliminates overlap of variables, e.g., \mat{$Knows(z_{17},OJ)$}


%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Generalized Modus Ponens (GMP)}


\mat{\[\frac{{p_1}', \;\; {p_2}', \; \ldots, \; {p_n}', \;\;
( p_1 \land p_2 \land \ldots \land p_n \Rightarrow q)}{q\theta}
\qquad \bbox{where }{p_i}'\theta \eq p_i\theta\bbox{ for all } i
\]}
\mat{\begin{formula}
{p_1}'  \bbox{ is }  King(John)  & p_1 \bbox{ is }  King(x) \\
{p_2}' \bbox{ is }  Greedy(y)  & p_2  \bbox{ is }  Greedy(x) \\
\theta  \bbox{ is }  \{x/John,y/John\} & q \bbox{ is } Evil(x) \\
q\theta \bbox{ is } Evil(John)
\end{formula}}

GMP used with KB of \defn{definite clauses} (\emph{exactly} one positive literal)\\
All variables assumed universally quantified

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Soundness of GMP}

Need to show that 
\mat{\[{p_1}', \; \ldots, \; {p_n}', \;\;
( p_1 \land \ldots \land p_n \Rightarrow q) \models q\theta\]}
provided that \mat{${p_i}'\theta \eq p_i\theta$} for all \mat{$i$}

Lemma: For any definite clause \mat{$p$}, we have \mat{$p \models p\theta$} by UI

1. \mat{$( p_1 \land \ldots \land p_n \Rightarrow q) \models 
    ( p_1 \land \ldots \land p_n \Rightarrow q)\theta \eq
    ( p_1\theta \land \ldots \land p_n\theta \Rightarrow q\theta)$}

2. \mat{$ {p_1}', \; \ldots, \; {p_n}' \models
     {p_1}' \land \ldots \land {p_n}' \models
     {p_1}'\theta \land \ldots \land {p_n}'\theta $}

3. From 1 and 2, \mat{$q\theta$} follows by ordinary Modus Ponens

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Example knowledge base}

The law says that it is a crime for an American to sell weapons to
hostile nations.  The country Nono\index{Nono}, an enemy of America,
has some missiles, and all of its missiles were sold to it by Colonel
West, who is American.

Prove that Col.~West is a criminal

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Example knowledge base contd.}

$\ldots$ it is a crime for an American to sell weapons to hostile nations:

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Example knowledge base contd.}

$\ldots$ it is a crime for an American to sell weapons to hostile nations:\al
  \mat{$American(x) \land  Weapon(y)\land Sells(x,y,z) \land  Hostile(z) \implies Criminal(x)$}\\
Nono $\ldots$ has some missiles

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Example knowledge base contd.}

$\ldots$ it is a crime for an American to sell weapons to hostile nations:\al
  \mat{$American(x) \land  Weapon(y)\land Sells(x,y,z) \land  Hostile(z) \implies Criminal(x)$}\\
Nono $\ldots$ has some missiles, i.e., $\exists\,x\ Owns(Nono,x)\land Missile(x)$:\al
  \mat{$Owns(Nono,M_1)$} and \mat{$Missile(M_1)$}\\
$\ldots$ all of its missiles were sold to it by Colonel West

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Example knowledge base contd.}

$\ldots$ it is a crime for an American to sell weapons to hostile nations:\al
  \mat{$American(x) \land  Weapon(y)\land Sells(x,y,z) \land  Hostile(z) \implies Criminal(x)$}\\
Nono $\ldots$ has some missiles, i.e., $\exists\,x\ Owns(Nono,x)\land Missile(x)$:\al
  \mat{$Owns(Nono,M_1)$} and \mat{$Missile(M_1)$}\\
$\ldots$ all of its missiles were sold to it by Colonel West\al
  \mat{$\All{x} Missile(x) \land Owns(Nono,x) \implies Sells(West,x,Nono)$}\\
Missiles are weapons:

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Example knowledge base contd.}

$\ldots$ it is a crime for an American to sell weapons to hostile nations:\al
  \mat{$American(x) \land  Weapon(y)\land Sells(x,y,z) \land  Hostile(z) \implies Criminal(x)$}\\
Nono $\ldots$ has some missiles, i.e., $\exists\,x\ Owns(Nono,x)\land Missile(x)$:\al
  \mat{$Owns(Nono,M_1)$} and \mat{$Missile(M_1)$}\\
$\ldots$ all of its missiles were sold to it by Colonel West\al
  \mat{$\All{x} Missile(x) \land Owns(Nono,x) \implies Sells(West,x,Nono)$}\\
Missiles are weapons:\al
  \mat{$Missile(x)\Rightarrow Weapon(x)$}\\
An enemy of America counts as ``hostile'':

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Example knowledge base contd.}

$\ldots$ it is a crime for an American to sell weapons to hostile nations:\al
  \mat{$American(x) \land  Weapon(y)\land Sells(x,y,z) \land  Hostile(z) \implies Criminal(x)$}\\
Nono $\ldots$ has some missiles, i.e., $\exists\,x\ Owns(Nono,x)\land Missile(x)$:\al
  \mat{$Owns(Nono,M_1)$} and \mat{$Missile(M_1)$}\\
$\ldots$ all of its missiles were sold to it by Colonel West\al
  \mat{$\All{x} Missile(x) \land Owns(Nono,x) \implies Sells(West,x,Nono)$}\\
Missiles are weapons:\al
  \mat{$Missile(x)\Rightarrow Weapon(x)$}\\
An enemy of America counts as ``hostile'':\al
  \mat{$Enemy(x,America)\implies Hostile(x)$}\\
West, who is American $\ldots$\al
  \mat{$American(West)$}\\
The country Nono, an enemy of America $\ldots$\al
  \mat{$Enemy(Nono,America)$}

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Forward chaining algorithm}

\input{algorithms/forward-chaining-algorithm}



%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Forward chaining proof}

\vspace*{0.2in}

\epsfxsize=1.08\maxfigwidth
\fig{\file{figures}{crime-fc1c.ps}}


%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Forward chaining proof}

\vspace*{0.2in}

\epsfxsize=1.08\maxfigwidth
\fig{\file{figures}{crime-fc2c.ps}}


%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Forward chaining proof}

\vspace*{0.2in}

\epsfxsize=1.08\maxfigwidth
\fig{\file{figures}{crime-fc3c.ps}}

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Properties of forward chaining}

Sound and complete for first-order definite clauses\\
(proof similar to propositional proof)

\defn{Datalog} = first-order definite clauses + \emph{no functions} (e.g., crime KB)\\
FC terminates for Datalog in poly iterations: at most \mat{$p\cdot n^k$} literals

May not terminate in general if \mat{$\alpha$} is not entailed

This is unavoidable: entailment with definite clauses is semidecidable

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Efficiency of forward chaining}

Simple observation: no need to match a rule on iteration \mat{$k$}\\
if a premise wasn't added on iteration \mat{$k-1$}\nl
$\implies$ match each rule whose premise contains a newly added literal

Matching itself can be expensive

\defn{Database indexing} allows \mat{$O(1)$} retrieval of known facts\al
e.g., query \mat{$Missile(x)$} retrieves \mat{$Missile(M_1)$}

Matching conjunctive premises against known facts is NP-hard

Forward chaining is widely used in \defn{deductive databases}

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Hard matching example}

\begin{minipage}[c]{0.42\maxfigwidth}
\epsfxsize=0.4\maxfigwidth
\centerline{\epsffile{figures/australia-csp.ps}}
\end{minipage}%
\hfill
\begin{minipage}[c]{0.58\maxfigwidth}
\noindent 
\tab\mat{$\Diff(wa,nt)\land \Diff(wa,sa)\land{}$}
\\[4pt]
\tab\tab\tab\mat{$\Diff(nt,q) \Diff(nt,sa)\land {}$}
\\[4pt]
\tab\tab\tab\mat{$\Diff(q,nsw)\land \Diff(q,sa)\land {}$}
\\[4pt]
\tab\tab\tab\mat{$\Diff(nsw,v)\land \Diff(nsw,sa)\land {}$}
\\[4pt]
\tab\tab\tab\mat{$\Diff(v,sa) \implies Colorable()$}
\\[8pt]
\tab\mat{$\Diff(Red,Blue) \quad \Diff(Red,Green)$}
\\[4pt]
\tab\mat{$\Diff(Green,Red)\quad \Diff(Green,Blue)$}
\\[4pt]
\tab\mat{$\Diff(Blue,Red) \quad \Diff(Blue,Green)$}
\end{minipage}

\mat{$Colorable()$} is inferred iff the CSP has a solution\\
CSPs include 3SAT as a special case, hence matching is NP-hard

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Backward chaining algorithm}

\input{algorithms/backward-chaining-algorithm}


%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Backward chaining example}

\vspace*{0.2in}

\epsfxsize=1.06\textwidth
\fig{\file{figures}{crime-bc01c.ps}}

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Backward chaining example}

\vspace*{0.2in}

\epsfxsize=1.06\textwidth
\fig{\file{figures}{crime-bc02c.ps}}

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Backward chaining example}

\vspace*{0.2in}

\epsfxsize=1.06\textwidth
\fig{\file{figures}{crime-bc03c.ps}}

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Backward chaining example}

\vspace*{0.2in}

\epsfxsize=1.06\textwidth
\fig{\file{figures}{crime-bc04c.ps}}

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Backward chaining example}

\vspace*{0.2in}

\epsfxsize=1.06\textwidth
\fig{\file{figures}{crime-bc05c.ps}}

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Backward chaining example}

\vspace*{0.2in}

\epsfxsize=1.06\textwidth
\fig{\file{figures}{crime-bc06c.ps}}

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Backward chaining example}

\vspace*{0.2in}

\epsfxsize=1.06\textwidth
\fig{\file{figures}{crime-bc07c.ps}}

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Properties of backward chaining}

Depth-first recursive proof search: space is linear in size of proof

Incomplete due to infinite loops\al
$\implies$ fix by checking current goal against every goal on stack

Inefficient due to repeated subgoals (both success and failure)\al
$\implies$ fix using caching of previous results (extra space!)

Widely used (without improvements!) for \defn{logic programming}

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Logic programming}

Sound bite: computation as inference on logical KBs

\begin{tabular}{lll}
    & \note{Logic programming}        & \note{Ordinary programming}     \\
1.  & Identify problem             & Identify problem             \\
2.  & Assemble information         & Assemble information         \\
3.  & Tea break                    & Figure out solution          \\
4.  & Encode information in KB     & Program solution             \\
5.  & Encode problem instance as facts & Encode problem instance as data  \\
6.  & Ask queries                  & Apply program to data \\
7.  & Find false facts             & Debug procedural errors \\
\end{tabular}

Should be easier to debug \mat{$Capital(NewYork,US)$} than \mat{$x:= x+2$} !






%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Prolog systems}

Basis: backward chaining with Horn clauses + bells \& whistles\\
Widely used in Europe, Japan (basis of 5th Generation project)\\
Compilation techniques $\Rightarrow$ approaching a billion LIPS

Program = set of clauses = {\tt head :- literal$_1$, $\ldots$ literal$_n$.}
\begin{LARGE}\begin{verbatim}
   criminal(X) :- american(X), weapon(Y), sells(X,Y,Z), hostile(Z).
\end{verbatim}\end{LARGE}

Efficient unification by \defn{open coding}\\
Efficient retrieval of matching clauses by direct linking\\
Depth-first, left-to-right backward chaining\\
Built-in predicates for arithmetic etc., e.g., {\tt X is Y*Z+3}\\
Closed-world assumption (``negation as failure'')\al
   e.g., given {\tt alive(X) :- not dead(X).}\al
   {\tt alive(joe)} succeeds if {\tt dead(joe)} fails



%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Prolog examples}

Depth-first search from a start state {\tt X}:
\begin{verbatim}
dfs(X) :- goal(X).
dfs(X) :- successor(X,S),dfs(S).
\end{verbatim}
No need to loop over {\tt S}: {\tt successor} succeeds for each

Appending two lists to produce a third:
\begin{verbatim}
append([],Y,Y).                         
append([X|L],Y,[X|Z]) :- append(L,Y,Z). 
                                        
query:   append(A,B,[1,2]) ?            
answers: A=[]    B=[1,2]
         A=[1]   B=[2]
         A=[1,2] B=[]
\end{verbatim}




%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Resolution: brief summary}

Full first-order version:
\mat{\[\frac {\ell_1 \lor \cdots\lor \ell_k,\qquad m_1 \lor \cdots\lor m_n}
        {(\ell_1 \lor \cdots\lor \ell_{i-1}\lor \ell_{i+1}\lor\cdots\lor \ell_k
        \lor m_1 \lor \cdots \lor m_{j-1}\lor m_{j+1}\lor\cdots\lor m_n)\theta}
\]}
where \mat{$\noprog{Unify}(\ell_i,\lnot m_j) \eq \theta$}.

For example,
\mat{\begin{formula}
{\begin{array}{l} \lnot Rich(x) \lor Unhappy(x) \\
                  Rich(Ken)
 \end{array}}
\over
{\begin{array}{l} Unhappy(Ken)
 \end{array}}
\end{formula}}
with \mat{$\theta = \{x/Ken\}$}

Apply resolution steps to \mat{$CNF(KB\land \lnot \alpha)$}; complete for FOL



%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Conversion to CNF}

Everyone who loves all animals is loved by someone:\al 
  \mat{$\All{x} [\All{y} Animal(y) \implies Loves(x,y)] \implies [\Exi{y} Loves(y,x)]$}

1. Eliminate biconditionals and implications
\mat{\[
 \All{x} [\lnot \All{y} \lnot Animal(y) \lor Loves(x,y)] \lor [\Exi{y} Loves(y,x)]
\]}
2. Move \mat{$\lnot$} inwards: \mat{$\lnot \All{x,p} \equiv \Exi{x} \lnot p$},\quad
                         \mat{$\lnot \Exi{x,p} \equiv \All{x} \lnot p$}:
\mat{\begin{formula}
 \All{x} [\Exi{y} \lnot(\lnot Animal(y) \lor Loves(x,y))] \lor [\Exi{y} Loves(y,x)] \\
 \All{x} [\Exi{y} \lnot\lnot Animal(y) \land \lnot Loves(x,y)] \lor [\Exi{y} Loves(y,x)] \\
 \All{x} [\Exi{y} Animal(y) \land \lnot Loves(x,y)] \lor [\Exi{y} Loves(y,x)] 
\end{formula}}

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Conversion to CNF contd.}

3. Standardize variables: each quantifier should use a different one
\mat{\[
 \All{x} [\Exi{y} Animal(y) \land \lnot Loves(x,y)] \lor [\Exi{z} Loves(z,x)] 
\]}
4. Skolemize: a more general form of existential instantiation.\nl
   Each existential variable is replaced by a \defn{Skolem function}\nl
   of the enclosing universally quantified variables:
\mat{\[
 \All{x} [Animal(F(x)) \land \lnot Loves(x,F(x))] \lor Loves(G(x),x)
\]}
5. Drop universal quantifiers:
\mat{\[
 [Animal(F(x)) \land \lnot Loves(x,F(x))] \lor Loves(G(x),x)
\]}
6. Distribute \mat{$\land$} over \mat{$\lor$}:
\mat{\[
 [Animal(F(x)) \lor Loves(G(x),x)] \land [\lnot Loves(x,F(x)) \lor Loves(G(x),x)]
\]}

%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Resolution proof: definite clauses}

\vspace*{0.2in}

\epsfxsize=1.08\textwidth
\fig{\file{figures}{crime-resolution.ps}}



\end{huge} 
\end{document}

