\documentstyle[fleqn,epsf,aima-slides]{article}
\begin{document}
\begin{huge}
\titleslide{Industrial-strength inference}{Chapter 9.5--6, Chapters 8.1 and 10.2--3}
\sf
%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Outline}
\blob Completeness
\blob Resolution
\blob Logic programming
%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Completeness in FOL}
Procedure $i$ is complete if and only if
\[
KB \vdash_i \alpha \quad \mbox{{\rm whenever}} \quad KB \models \alpha
\]
Forward and backward chaining are \u{complete for Horn KBs}\\
but incomplete for general first-order logic
E.g., from
\begin{formula}
PhD(x) \implies HighlyQualified(x) \\
\lnot PhD(x) \implies EarlyEarnings(x)\\
HighlyQualified(x) \implies Rich(x)\\
EarlyEarnings(x) \implies Rich(x)
\end{formula}
should be able to infer $Rich(Me)$, but FC/BC won't do it
Does a complete algorithm exist?
%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{A brief history of reasoning}
\begin{tabular}{lll}
450{\sc b.c.} & Stoics & propositional logic, inference (maybe) \\
322{\sc b.c.} & Aristotle & ``syllogisms'' (inference rules), quantifiers \\
1565 & Cardano & probability theory (propositional logic + uncertainty) \\
1847 & Boole & propositional logic (again) \\
1879 & Frege & first-order logic \\
1922 & Wittgenstein& proof by truth tables \\
1930 & G\"odel & $\exists$ complete algorithm for FOL \\
1930 & Herbrand & complete algorithm for FOL (reduce to propositional) \\
1931 & G\"odel & $\lnot\exists$ complete algorithm for arithmetic \\
1960 & Davis/Putnam& ``practical'' algorithm for propositional logic \\
1965 & Robinson & ``practical'' algorithm for FOL---resolution
\end{tabular}
%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Resolution}
Entailment in first-order logic is only \u{semidecidable}:\al
can find a proof of $\alpha$ if $KB \models \alpha$\al
cannot always prove that $KB \not\models \alpha$\\
Cf. Halting Problem: proof procedure may be about to terminate
with success or failure, or may go on for ever
Resolution is a \u{refutation} procedure:\al
to prove $KB \models \alpha$, show that $KB\land\lnot\alpha$ is unsatisfiable
Resolution uses $KB$, $\lnot\alpha$ in CNF (conjunction of clauses)
Resolution inference rule combines two clauses to make a new one:
\vspace*{0.15in}
\epsfxsize=2in
\fig{\file{figures}{resolve-clauses.ps}}
Inference continues until an \u{empty clause} is derived (contradiction)
%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Resolution inference rule}
Basic propositional version:
\begin{formula}
{\displaystyle
\frac{\alpha \lor \beta,\;\; \lnot \beta \lor \gamma}{\alpha \lor \gamma}
\qquad \mbox{or equivalently} \qquad
\frac{\lnot\alpha \implies \beta,\;\; \beta \implies \gamma}{\lnot \alpha \implies \gamma}
}
\end{formula}
Full first-order version:
\begin{formula}
{\begin{array}{l} p_1\lor \ldots\ p_j\ \ldots \lor p_m,\\
q_1\lor \ldots\ q_k\ \ldots \lor q_n
\end{array}}
\over
{\begin{array}{l}
(p_1\lor \ldots\ p_{j-1} \lor p_{j+1}\ \ldots p_m \lor
q_1\ldots\ q_{k-1} \lor q_{k+1}\ \ldots \lor q_n)\sigma
\end{array}}
\end{formula}
where $p_j\sigma = \lnot q_k \sigma$
For example,
\begin{formula}
{\begin{array}{l} \lnot Rich(x) \lor Unhappy(x) \\
Rich(Me)
\end{array}}
\over
{\begin{array}{l} Unhappy(Me)
\end{array}}
\end{formula}
with $\sigma = \{x/Me\}$
%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Conjunctive Normal Form}
\u{Literal} = (possibly negated) atomic sentence, e.g., $\lnot Rich(Me)$
\u{Clause} = disjunction of literals, e.g., $\lnot Rich(Me) \lor Unhappy(Me)$
The KB is a conjunction of clauses
Any FOL KB can be converted to CNF as follows:\\
1. Replace $P{\implies}Q$ by ${\lnot}P{\lor}Q$\\
2. Move $\lnot$ inwards, e.g.,
$\lnot \forall x\,P$ becomes $\exists x\,\lnot P$\\
3. Standardize variables apart, e.g.,
$\forall x\,P \lor \exists x\,Q$ becomes $\forall x\,P \lor \exists y\,Q$\\
4. Move quantifiers left in order, e.g.,
$\forall x\,P \lor \exists x\,Q$ becomes $\forall x\exists y\,P \lor Q$\\
5. Eliminate $\exists$ by Skolemization (next slide)\\
6. Drop universal quantifiers\\
7. Distribute $\land$ over $\lor$, e.g.,
$(P \land Q) \lor R$ becomes $(P\lor Q) \land (P\lor R)$
%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Skolemization}
$\exists x\,Rich(x)$ becomes $Rich(G1)$ where $G1$ is a new ``\u{Skolem constant}''
$\Exi{k} \frac{d}{dy}(k^y) \eq k^y$ becomes $\frac{d}{dy}(e^y) \eq e^y$
More tricky when $\exists$ is inside $\forall$
E.g., ``Everyone has a heart''\al
$\All{x} Person(x) \implies \Exi{y} Heart(y) \land Has(x,y)$
\u{Incorrect}:\al
$\All{x} Person(x) \implies Heart(H1) \land Has(x,H1)$
\u{Correct}:\al
$\All{x} Person(x) \implies Heart(H(x)) \land Has(x,H(x))$\\
where $H$ is a new symbol (``Skolem function'')
Skolem function arguments: all \u{enclosing} universally quantified variables
%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Resolution proof}
To prove $\alpha$:\al
-- negate it\al
-- convert to CNF\al
-- add to CNF KB\al
-- infer contradiction
E.g., to prove $Rich(me)$, add $\lnot Rich(me)$ to the CNF KB
\begin{formula}
\lnot PhD(x) \lor HighlyQualified(x) \\
PhD(x) \lor EarlyEarnings(x)\\
\lnot HighlyQualified(x) \lor Rich(x)\\
\lnot EarlyEarnings(x) \lor Rich(x)
\end{formula}
%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Resolution proof}
\vspace*{0.3in}
\epsfxsize=1.0\textwidth
\fig{\file{figures}{rich-proof.ps}}
%%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\heading{Resolution in practice}
%
%Resolution is complete and usually necessary for mathematics
%
%Automated theorem provers are starting to be useful to mathematicians
%and have proved several new theorems
%%%%%%%%%%%% Slide %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\heading{Logic programming}
Sound bite: computation as inference on logical KBs
\begin{tabular}{lll}
& \u{Logic programming} & \u{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 $Capital(NewYork,US)$ than $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$ 10 million LIPS
Program = set of clauses = {\tt head :- literal$_1$, $\ldots$ literal$_n$.}\\
Efficient unification by \u{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., {\tt not PhD(X)} succeeds if {\tt PhD(X)} 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}
\end{huge}
\end{document}