\documentstyle[fleqn,epsf,aima-slides]{article}
\begin{document}
\begin{huge}
\titleslide{Inference in first-order logic}{Chapter 9, Sections 1--4}
\sf
%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Outline}
\blob Proofs
\blob Unification
\blob Generalized Modus Ponens
\blob Forward and backward chaining
%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Proofs}
Sound inference: find $\alpha$ such that $KB \models \alpha$.\\
Proof process is a \u{search}, operators are inference rules.
E.g., Modus Ponens (MP)
\[\displaystyle
\frac{\alpha,\quad \alpha\implies\beta}{\beta} \qquad
\frac{At(Joe,UCB)\quad At(Joe,UCB)\implies OK(Joe)}{OK(Joe)}
\]
E.g., And-Introduction (AI)
\[\displaystyle
\frac{\alpha \quad \beta}{\alpha \land \beta} \qquad
\frac{OK(Joe)\quad CSMajor(Joe)}{OK(Joe)\land CSMajor(Joe)}
\]
E.g., Universal Elimination (UE)
\[\displaystyle
\frac{\All{x} \alpha}{\alpha\{x/\tau\}} \qquad
\frac{\All{x} At(x,UCB)\implies OK(x)}{At(Pat,UCB)\implies OK(Pat)}
\]
$\tau$ must be a ground term (i.e., no variables)
%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Example proof}
\begin{tabular}{l|ll}
Bob is a buffalo & 1. & $Buffalo(Bob)$ \\
Pat is a pig & 2. & $Pig(Pat)$ \\
Buffaloes outrun pigs & 3. & $\All{x,y} Buffalo(x) \land Pig(y) \implies Faster(x,y)$\\
\hline
Bob outruns Pat & &\phantom{$Buffalo(Bob) \land Pig(Pat) \implies Faster(Bob,Pat)$}\\
\phantom{UE 3, $\{x/Bob,y/Pat\}$} & & \\
\end{tabular}
%%%%%%%%%%%% Overlay %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\pheading{Example proof}
\begin{tabular}{l|ll}
\phantom{Bob is a buffalo} & & \\
\phantom{UE 3, $\{x/Bob,y/Pat\}$} & & \\
\phantom{Buffaloes outruns pigs} & & \\
\hline
\phantom{Bob outruns Pat} & & \phantom{$Buffalo(Bob) \land Pig(Pat) \implies Faster(Bob,Pat)$}\\
\hline
AI 1 \& 2 & 4. & $Buffalo(Bob) \land Pig(Pat)$ \\
\end{tabular}
%%%%%%%%%%%% Overlay %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\pheading{Example proof}
\begin{tabular}{l|ll}
\phantom{Bob is a buffalo} & & \\
\phantom{Pat is a pig} & & \\
\phantom{Buffaloes outrun pigs} & & \\
\hline
\phantom{Bob outruns Pat} & & \phantom{$Buffalo(Bob) \land Pig(Pat) \implies Faster(Bob,Pat)$}\\
\hline
\phantom{AI 1 \& 2} & & \\
UE 3, $\{x/Bob,y/Pat\}$ & 5. & $Buffalo(Bob) \land Pig(Pat) \implies Faster(Bob,Pat)$\\
\end{tabular}
%%%%%%%%%%%% Overlay %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\pheading{Example proof}
\begin{tabular}{l|ll}
\phantom{Bob is a buffalo} & & \\
\phantom{Pat is a pig} & & \\
\phantom{Buffaloes outrun pigs} & & \\
\hline
\phantom{Bob outruns Pat} & & \phantom{$Buffalo(Bob) \land Pig(Pat) \implies Faster(Bob,Pat)$} \\
\hline
\phantom{AI 1 \& 2} & & \\
\phantom{UE 3, $\{x/Bob,y/Pat\}$} & & \\
MP 6 \& 7 & 6. & $Faster(Bob,Pat)$ \\
\end{tabular}
%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Search with primitive inference rules}
Operators are inference rules\\
States are sets of sentences\\
Goal test checks state to see if it contains query sentence
\begin{tabular}{lr}
\epsfxsize=0.3\textwidth
\epsffile{\file{figures}{naive-proof-tree.ps}}
&
\hbox{\begin{minipage}[b]{0.65\textwidth}
AI, UE, MP is a common inference pattern\\
\u{Problem}: branching factor huge, esp.~for UE\\
\u{Idea}: find a substitution that makes the rule premise match some
known facts\al
$\Rightarrow$ a single, more powerful inference rule
\end{minipage}}
\end{tabular}
%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Unification}
A substitution $\sigma$ unifies atomic sentences $p$ and $q$ if
\u{\u{$p\sigma = q\sigma$}}
\[\begin{array}{l|l|l}
p & q & \sigma \\
\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)\}}\\
\end{array}\]
%%%%%%%%%%%% Overlay %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\pheading{Unification}
.
\[\begin{array}{l|l|l}
& & \\
\hline
\phantom{Knows(John,x)} & \phantom{Knows(John,Jane)} & \{x/Jane\}\\
\phantom{Knows(John,x)} & \phantom{Knows(y,OJ)} & \{x/John,y/OJ\}\\
\phantom{Knows(John,x)} & \phantom{Knows(y,Mother(y)}& \{y/John,x/Mother(John)\}\\
\end{array}\]
\u{Idea}: Unify rule premises with known facts, apply unifier to conclusion\\
\begin{tabular}{rl}
E.g., if we know $q$ and & $Knows(John,x) \implies Likes(John,x)$ \\
then we conclude & $Likes(John,Jane)$ \\
& $Likes(John,OJ)$ \\
& $Likes(John,Mother(John))$
\end{tabular}
%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Generalized Modus Ponens (GMP)}
\[\frac{{p_1}', \;\; {p_2}', \; \ldots, \; {p_n}', \;\;
( p_1 \land p_2 \land \ldots \land p_n \Rightarrow q)}{q\sigma}
\qquad \mbox{where }{p_i}'\sigma \eq p_i\sigma\mbox{ for all } i
\]
\begin{tabular}{rl}
E.g. ${p_1}'\eq$ & Faster(Bob,Pat) \\
${p_2}'\eq$ & Faster(Pat,Steve) \\
$p_1 \land p_2 \implies q\ \eq$ & $Faster(x,y) \land Faster(y,z) \implies Faster(x,z)$ \\
$\sigma\eq$ & $\{x/Bob,y/Pat,z/Steve\}$ \\
$q\sigma\eq$ & $Faster(Bob,Steve)$ \\
\end{tabular}
GMP used with KB of \u{definite clauses} ({\em exactly} one positive literal):\\
either a single atomic sentence or\nl
(conjunction of atomic sentences) $\Rightarrow$ (atomic sentence)\\
All variables assumed universally quantified
%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Soundness of GMP}
Need to show that
\[{p_1}', \; \ldots, \; {p_n}', \;\;
( p_1 \land \ldots \land p_n \Rightarrow q) \models q\sigma\]
provided that ${p_i}'\sigma \eq p_i\sigma$ for all $i$
Lemma: For any definite clause $p$, we have $p \models p\sigma$ by UE
1. $( p_1 \land \ldots \land p_n \Rightarrow q) \models
( p_1 \land \ldots \land p_n \Rightarrow q)\sigma \eq
( p_1\sigma \land \ldots \land p_n\sigma \Rightarrow q\sigma)$
2. $ {p_1}', \; \ldots, \; {p_n}' \models
{p_1}' \land \ldots \land {p_n}' \models
{p_1}'\sigma \land \ldots \land {p_n}'\sigma $
3. From 1 and 2, $q\sigma$ follows by simple MP
%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Forward chaining}
When a new fact $p$ is added to the KB\al
for each rule such that $p$ unifies with a premise\nl
if the other premises are \u{known}\nl
then add the conclusion to the KB and continue chaining
Forward chaining is \u{data-driven}\nl
e.g., inferring properties and categories from percepts
%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Forward chaining example}
Add facts 1, 2, 3, 4, 5, 7 in turn.\\
Number in [] = unification literal; \tick\ indicates rule firing
\u{1.} $Buffalo(x) \land Pig(y) \implies Faster(x,y)$\\
\u{2.} $Pig(y) \land Slug(z) \implies Faster(y,z)$\\
\u{3.} $Faster(x,y) \land Faster(y,z) \implies Faster(x,z)$\\
\u{4.} $Buffalo(Bob)$ \u{[1a,\cross]}\\
\u{5.} $Pig(Pat)$ \u{[1b,\tick]} $\rightarrow$ \u{6.} $Faster(Bob,Pat)$ \u{[3a,\cross]}, \u{[3b,\cross]}\\
\phantom{\u{5.} $Pig(Pat)$} \u{[2a,\cross]}\\
\u{7.} $Slug(Steve)$ \u{[2b,\tick]}\al
$\rightarrow$\u{8.} $Faster(Pat,Steve)$ \u{[3a,\cross]}, \u{[3b,\tick]}\nl
$\rightarrow$\u{9.} $Faster(Bob,Steve)$ \u{[3a,\cross]}, \u{[3b,\cross]}
%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Backward chaining}
When a query $q$ is asked\al
if a matching fact $q'$ is known, return the unifier\al
for each rule whose consequent $q'$ matches $q$\nl
attempt to prove each premise of the rule by backward chaining
(Some added complications in keeping track of the unifiers)
(More complications help to avoid infinite loops)
Two versions: find \u{any} solution, find \u{all} solutions
Backward chaining is the basis for \u{logic programming}, e.g., Prolog
%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Backward chaining example}
\u{1.} $Pig(y) \land Slug(z) \implies Faster(y,z)$\\
\u{2.} $Slimy(z) \land Creeps(z) \implies Slug(z)$\\
\u{3.} $Pig(Pat)$ \qquad \u{4.} $Slimy(Steve)$ \qquad \u{5.} $Creeps(Steve)$
\vspace*{0.4in}
\epsfxsize=0.6\textwidth
\fig{\file{figures}{slug-bc.ps}}
\end{huge}
\end{document}