%! TEX program = xelatex
\documentclass[aspectratio=169]{beamer}
\usepackage{amsthm}
\usepackage{graphicx}
\usepackage{fancybox}
\usepackage{listings}
\input{../common/fontsetup}
\input{../common/scalalistings}
\input{../common/mathsetup}

\input{../common/mysymbols}
\input{../common/constructors} 
\input{../common/mybeamer}

\usepackage{tikz}
\usetikzlibrary{automata,positioning,arrows,arrows.meta}
\usepackage{bclogo}

\title{Automating First-Order Logic Proofs Using Resolution}
\author{Viktor Kun\v{c}ak, EPFL}
\date{} %\url{https://lara.epfl.ch/w/fv}}

\nobox
\begin{document}
\maketitle

\begin{frame}{Automating first-order logic (FOL)}

First-order logic supports arbitrary (uninterpreted) predicates and functions
\begin{itemize}
\item their meaning will be constrained through axioms
\end{itemize}

\

FOL can be used in practice to formalize most of mathematics (e.g. through set theory axioms),
and thus all of program verification problems.

To prove whether a property holds, we can proceed as follows:
\begin{itemize}
\item describe the property using a formula $F$ 
\item describe the functions and relations in $F$ using a sequence of axioms $S$
\end{itemize}
Check if the sequence $(\lnot F; S)$ is contradictory. If yes, then $F$ follows from $S$

\ \\

Completeness: there is a procedure that will, if $F$ does follow from $S$, in finite time
establish this (we do not know how long it will take, if it does not hold, it loops).
%% \begin{itemize}
%% \item semantic notion $S \models F$ (in all interpretations $S$ formula $F$ is true) can, 
%% in first-order logic, be replaced with syntactic notion (can we derive a contradiction)
%% \end{itemize}

We give one such procedure: resolution for FOL.
\end{frame}

\begin{frame}{Running example of FOL formula}

  Here is a first-order logic formula:
\[
\begin{array}{l@{}l}
  & \big[(\forall x. \exists y.\ R(x,y))\ \land \\
      & (\forall x. \forall y.\ (R(x,y) \rightarrow \forall z.\ R(x,f(y,z))))\ \land \\
      & (\forall x.\ (P(x) \lor P(f(x,a))))\big]\ \\
      & \rightarrow \forall x. \exists y.\ (R(x,y) \land P(y))
\end{array}
\]
Note that it contains:
\begin{itemize}
\item propositional operations $\land, \lor, \lnot, \rightarrow$
\item variables $x, y$
\item function symbols and constants: $f, a$
\item predicate symbols: $P, R$
\item quantifiers $\forall,\exists$ (only over variables, not function or predicate symbols - FO)
\end{itemize}
  
\end{frame}

\begin{frame}
  \frametitle{First-order logic syntax and terminology}

  A first-order \emph{signature} ${\cal L}$ (akka language) specifies a countable set of function symbols $f$ (constants $c$ are functions symbols taking no arguments), and predicate symbols $p$.
  
  Syntax of formulas ($F$) and terms ($t$) in first-order logic:
  \[\begin{array}{l}
  F ::= p(t_1,\ldots,t_n) \mid \forall x. F \mid \exists x. F \mid \top \mid \bot \mid
      \lnot F \mid F_1 \land F_2 \mid F_1 \lor F_2 \mid F_1 \rightarrow F_2 \mid F_1 \leftrightarrow F_2 \\
      t ::= x \mid c \mid f(t_1,\ldots,t_n)
    \end{array}\]
  where $x \in Var$ denotes variables, which form a countably infinite fixed set.

  $ar$ denotes arity of functions and predicate symbols; e.g. $ar(f)=2$ means $f$ takes two arguments, so
  it is allowed to form a term $f(t_1,t_2)$, and also $ar(p)=2$ for predicate symbol $p$ means that
  it is allowed to form formula $p(t_1,t_2)$.

  We interpret each $f$ as $\bar f : D^{ar(f)} \to D$ and each $p$ as $\bar p : D^{ar(p)} \to \{ 0, 1 \}$
  (or: $\subseteq D^{ar(p)}$)

  \

  We call $p(t_1,\ldots,t_n)$ an \emph{atomic formula} (contains no logical connectives or quantifiers).

  A \emph{literal} is such an atomic formula, or its negation $\lnot p(t_1,\ldots,t_n)$

  A \emph{clause} is a disjunction of literals, e.g. $\lnot p(x,f(y)) \lor q(y) \lor \lnot r(x,z)$
\end{frame}

\begin{frame}{Example of a FOL signature}

We will look at the signature ${\cal L} = \{P, R, a, f\}$ where
\begin{itemize}
\item $P$ is a predicate symbol, $ar(P)=1$
\item $R$ is a predicate symbol, $ar(R)=2$
\item $a$ is a constant
\item $f$ is a function symbol, $ar(f)=2$
\end{itemize}

An \textbf{interpretation} for this language is then any structure $(D,e)$ where 
\begin{itemize}
\item $D \ne \emptyset$ (it can be finite or infinite)
\item $e(P) : D \to \{0,1\}$
\item $e(R) : D^2 \to \{0,1\}$
\item $e(a) \in D$
\item $e(f): D^2 \to D$
\end{itemize}
Example: $D = \{ 0, 1, 2, \dots \}$ (non-negative integers) and:
\begin{itemize}
\item $e(P)(n) = \mbox{ if } (2|n) \mbox{ then } 1 \mbox{ else } 0$
\item $e(R)(x,y)  = \mbox{ if } (x \le y) \mbox{ then } 1 \mbox{ else } 0$
\item $e(a) = 1$
\item $e(f)(x,y) = x + y$
\end{itemize}
\end{frame}

\begin{frame}{Semantics given an interpretation}
Taking that interpretation, $D = \{ 0, 1, 2, \dots \}$,
\begin{itemize}
\item $e(P)(n) = \mbox{ if } (2|n) \mbox{ then } 1 \mbox{ else } 0$
\item $e(R)  = \mbox{ if } (x \le y) \mbox{ then } 1 \mbox{ else } 0$
\item $e(a) = 1$
\item $e(f)(x,y) = x + y$
\end{itemize}
we can talk about the truth value of any closed formula, e.g.:
\[
\begin{array}{l@{\hspace*{1cm}}l}
  \mbox{ (text, or tree) } &
\begin{array}{l@{}l}
  & (\forall x. \exists y.\ R(x,y))\ \land \\
      & (\forall x. \forall y.\ (R(x,y) \rightarrow \forall z.\ R(x,f(y,z))))\ \land \\
      & (\forall x.\ (P(x) \lor P(f(x,a))))\ \\
      & \rightarrow \forall x. \exists y.\ (R(x,y) \land P(y))
\end{array}
\end{array}
\]
Its truth is precisely the truth of this (symbols are replaced with their value in $e$):
\[
\begin{array}{l@{\hspace*{1cm}}l}
  \mbox{(true or false)} &
\begin{array}{l@{}l}
  & (\forall x. \exists y.\ x \le y)\ \land \\
      & (\forall x. \forall y.\  x \le y\  \rightarrow \forall z.\ x \le (y + z))\ \land \\
      & (\forall x.\ (2|x) \lor (2| x + 1))\ \\
      & \rightarrow \forall x. \exists y.\ (x \le y \land (2|y))
\end{array}
\end{array}
\]
\end{frame}

\begin{frame}
  \frametitle{Semantics in general: interpreter written in set theory}

  A first-order \emph{interpretation}
  is $I=(D,e)$ where $D \neq \emptyset$ and $e$ maps constants, function and predicate symbols
  as follows:
  \begin{itemize}
  \item each predicate symbol $p$ with $ar(p)=n$ into $e(p) : D^n \to \{ 0, 1 \}$
  \item each function symbol $f$ with $ar(f)=n$ into a total function of $n$ arguments, $e(f) : D^n \to D$
    (and each constant $c$ into element of $D$, i.e., $e(c) \in D$)
  \item maps each variable $x$ to element of $D$, i.e., $e(x) \in D$
  \end{itemize}

  We then define $\tr{F}_{I} \in \{ 0, 1 \}$ to denote whether $F$ is true ($1$) or false
  ($0$) false in interpretation $I$.
  The rules are the expected rules recursive on the formula tree:
  
  \[  
    \tr{F_1 \land F_2}_I = \tr{F_1}_I \land \tr{F_2}_I     \hspace{1cm}
    \tr{F_1 \lor F_2}_I = \tr{F_1}_I \lor \tr{F_2}_I     \hspace{1cm}
    \tr{\lnot F}_I = \lnot \tr{F}_I \hspace{1cm}
    \tr{\bot}_I = 0
  \]
  \[
    \tr{f(t_1,\ldots,t_n)}_I = e(f)(\tr{t_1}_I, \ldots, \tr{t_n}_I) \hspace{0.5cm}
    \tr{p(t_1,\ldots,t_n)}_I = e(p)(\tr{t_1}_I, \ldots, \tr{t_n}_I) \hspace{0.5cm}
    \tr{x}_I = e(x) 
  \]
  \[
  \begin{array}{l}
  \tr{\forall x. F}_{(D,e)} = \mbox{ if } (\forall d \in D.\ (\tr{F}_{(D,e[x:=d])}=1))
                             \mbox{ then } 1 \mbox{ else } 0 \\
  \tr{\exists x. F}_{(D,e)} = \mbox{ if } (\exists d \in D.\ (\tr{F}_{(D,e[x:=d])}=1))
                            \mbox{ then } 1 \mbox{ else } 0 
  \end{array}
  \]
  where $e[x:=d](y) = (\mbox{if } x = y \mbox{ then } d \mbox{ else } e(y))$
\end{frame}

\begin{frame}
  \frametitle{What makes this logic first order}

  \[\begin{array}{c}
  \tr{\forall x. F}_{(D,e)} = \mbox{if} (\{ d \in D \mid \tr{F}_{(D,e[x:=d])} = 1 \} = D) \mbox{ then } 1
    \mbox{ else } 0 \\ 
  \tr{\exists x. F}_{(D,e)} = \mbox{if} (\{ d \in D \mid \tr{F}_{(D,e[x:=d])} = 1 \} \neq \emptyset) \mbox{ then } 1
  \mbox{ else } 0
  \end{array}\] 
  We \emph{can} quantify over variables $\forall x.F$, $\exists x.F$, which are interpreted over $D$,
  and we can nest quantifiers, e.g. $\forall x. \exists y.\ (p(x,y) \land q(y,x))$.

  We \emph{cannot} write a FOL formula that quantifies over function and relation symbols
  (that would be \emph{second-order} or, generally, \emph{higher-order}).

  \

  The meaning of function and relation symbols is fixed in $e$ of interpretation $I=(D,e)$.

  \
  
  To make statements that do not depend on a particular interpretation,
  we use concepts of \emph{satisfiability} and \emph{validity}:
  \begin{itemize}
  \item $F$ is \textbf{valid} if, \textbf{for all interpretations} $(D,e)$ \\
    (for arbitrarily small or large sets $D$ and all possible choices of $e$), $\tr{F}_{(D,e)} = 1$
  \item $F$ is \textbf{satisfiable} if \textbf{there exists an interpretation} $(D,e)$
    such that $\tr{F}_{(D,e)} = 1$
  \end{itemize} 
\end{frame}

\newcommand{\bp}{\overline{p}}
\newcommand{\bq}{\overline{q}}
\begin{frame}
  \frametitle{Satisfiability and validity: illustration}

  Take first-order logic (FOL) formula
  \[
      \forall x. \exists y.\ (p(x,y) \land q(y,x))
  \]
  Its \textbf{satisfiability} is, by definition, equivalent to an informal statement
  (which itself is not a formula of first-order logic but a (meta)mathematical statement):
  \[
    \mathbf{\exists D \neq \emptyset.\ \exists \bp,\bq : D^2 \to \{0,1\}}.\
       \forall x \in D. \exists y \in D.\ ((\bp(x,y) \land \bq(y,x))=1)
  \]
  Its \textbf{validity} is, by definition, equivalent a mathematical statement:
  \[
    \mathbf{\forall D \neq \emptyset.\ \forall \bp,\bq : D^2 \to \{0,1\}}.\
       \forall x \in D. \exists y \in D.\ ((\bp(x,y) \land \bq(y,x))=1)
  \]
  The domain, functions, and relations are either all existentially quantified (if we ask
  about satisfiability) or all universally quantified (if we ask about validity).

  \

  \textbf{Observation:} $F$ is valid if and only if $\lnot F$ is not satisfiable.

  We will be checking satisfiability (aiming for a negative answer).
\end{frame}

\begin{frame}
  \frametitle{Back to our example}
Consider our example formula $F$:
\begin{equation*}
\begin{array}{l@{}l}
  & (\forall x. \exists y.\ R(x,y))\ \land \\
      & (\forall x. \forall y.\ R(x,y) \rightarrow \forall z.\ R(x,f(y,z)))\ \land \\
      & (\forall x.\ P(x) \lor P(f(x,a)))\ \\
      & \rightarrow \forall x. \exists y.\ R(x,y) \land P(y)
\end{array}
\end{equation*}
We have seen it has an interpretation where it is true, so $F$ is satisfiable.

We are interested in checking its \emph{validity}.

To do that, we will check the satisfiability of $\lnot F$.
\begin{equation*}
\begin{array}{l@{}l}
\lnot \big( \ \ & (\forall x. \exists y.\ R(x,y))\ \land \\
      & (\forall x. \forall y.\ R(x,y) \rightarrow \forall z.\ R(x,f(y,z)))\ \land \\
      & (\forall x.\ P(x) \lor P(f(x,a)))\ \\
      & \rightarrow \forall x. \exists y.\ R(x,y) \land P(y) \ \big)
\end{array}
\end{equation*}
In general, we will transform $\lnot F$ into a \emph{normal form}.
\end{frame}

\begin{frame}
  \frametitle{Negation normal form for FOL}

  Observation:
  If $F \leftrightarrow G$ is a valid FOL formula,
  then inside any other FOL formula $H$ we can replace a sub-formula $F$ with $G$
  without changing the truth value of the formula: $H[F] \leadsto H[G]$.

  \ \\
  
  We can transform formulas to negation normal using transformations such as these:
  \[\begin{array}{rcl}
   F_1 \leftrightarrow F_2 &\leadsto& (F_1 \rightarrow F_2) \wedge (F_2 \rightarrow F_1) \\
   F_1 \rightarrow F_2 &\leadsto& \neg F_1 \vee F_2 \\
   \neg \neg F &\leadsto& F \\
   \neg (F_1 \wedge F_2) &\leadsto& \neg F_1 \vee \neg F_2 \\
   \neg (F_1 \vee F_2) &\leadsto& \neg F_1 \wedge \neg F_2 \\
   \neg \forall x.F &\leadsto& \exists x. \neg F \\
   \neg \exists x.F &\leadsto& \forall x. \neg F \\
   \neg \bot &\leadsto& \top \\
   \neg \top &\leadsto& \bot \\
    \end{array}\]
  In negation normal form, negation applies only to atomic formulas and the only other 
  propositional connectives are $\land$, $\lor$.  
\end{frame}

\begin{frame}
  \frametitle{Compute negation normal form}

  \begin{equation*}
\begin{array}{l@{}l}
\lnot \bigg( \big( & (\forall x. \exists y.\ R(x,y))\ \land \\
      & \big(\forall x. \forall y.\ (R(x,y) \rightarrow \forall z.\ R(x,f(y,z)))\big)\ \land \\
      & (\forall x.\ P(x) \lor P(f(x,a)))\ \big) \
      \rightarrow \forall x. \exists y.\ R(x,y) \land P(y) \bigg)
\end{array}
\end{equation*}

becomes: \pause
  
\begin{equation*}
\begin{array}{l@{}l}
 & (\forall x. \exists y.\ R(x,y))\ \land \\
      & \big(\forall x. \forall y.\ (\neg R(x,y) \lor \forall z.\ R(x,f(y,z)))\big)\ \land \\
      & \big(\forall x.\ (P(x) \lor P(f(x,a)))\big)\ \land \\
      & \big(\exists x. \forall y.\ (\neg R(x,y) \vee \neg P(y))\big)
\end{array}
\end{equation*}
\pause
Coming next: get rid of existential quantifiers!
\end{frame}

\begin{frame}
  \frametitle{Introducing a Skolem function}

  Observe that e.g. the following formula is valid: $p(x,s(x)) \ \rightarrow \ \exists y. p(x,y)$.

  Indeed, fix any interpretation $(D,e)$ and
  assume $p(x,s(x))$. 

  To prove $\exists y. p(x,y)$, just let $y$ be $s(x)$.

  Consequently, if $\forall x. p(x,s(x))$ is satisfiable, so is $\forall x. \exists y. p(x,y)$.

  A converse is also true. Take any interpretation $(D,e)$ in which
  $\forall x. \exists y. p(x,y)$ holds. Then for any $x_d$, there exists $y_d \in D$ such
  that $e(p)(x_d,y_d)=1$. Construct (by axiom of choice)
  a function $\bar s$ that assigns to every element $x_d \in D$ one such
  $y_d \in D$ for which $e(p)(x_d,y_d)=1$. 
  Extend the signature with a \textbf{new
    function symbol} $s$ \\
  (Skolem function, according to \wiki{Thoralf Skolem})
  that does not appear in the formula. Define a new interpretation $I'=(D,e')$ (with the
  same domain) by $e' = e[s:= \bar s]$, that is, $e'$ behaves like $e$ but maps a new symbol $s$ to
  the function $\bar s$.
  Then $\tr{\forall x. p(x,s(x))}_{I'} = 1$.

  We can do this transform of $\exists$ to Skolem functions 
  not just for $p$, but any quantifier-free formula. 
  The transformation preserves satisfiability.
\end{frame}

\begin{frame}
  \frametitle{Skolemization Algorithm in General}

  In a formula that is in negation normal form, replace a subformula
  \[
      \exists y.\ F(x_1,\ldots,x_n,y)
  \]
  with 
  \[
       F(x_1,\ldots,x_n,g(x_1,\ldots,x_n))
  \]
  where $g$ is a new function symbol (Skolem function) of arity $n$
  and $\{x_1,\ldots,x_n\}$ are the variables free in $F$, computed
  like this:
  \[\begin{array}{rcl}
      FV(c) &=& \emptyset, \ \ FV(x) = \{ x \} \\
      FV(f(t_1,\ldots,t_n)) &=& FV(t_1) \cup \ldots \cup FV(t_n) =  FV(p(t_1,\ldots,t_n)) \\
      FV(F_1 \land F_2) &=& FV(F_1) \cup FV(F_2)  \hspace{1.5cm}
      FV(\lnot F) = FV(F)  \\
      FV(\forall x. F) &=& FV(F) \setminus \{ x \} = FV(\exists x. F)
  \end{array}\]
  If we have quantifiers $Q_1 x_1. \ldots Q_n x_n. F$ we start eliminating from outside (left) and then
  Skolem function arguments for $\exists x_i$ are only $\forall$ quantified variables
  among $x_1,\ldots,x_{i-1}$.
\end{frame}

\newcommand{\sknote}[1]{\alert{#1}}
\newcommand{\sknotee}[1]{\phantom{\alert{#1}}}
\begin{frame}{Skolemized form for the example}

\begin{equation*}
\begin{array}{l@{}ll}
  & (\forall x. \exists y.\ R(x,y))\ \land
      & \sknote{y \leadsto s_1(x)} \\
  & \big(\forall x. \forall y.\ (\neg R(x,y) \lor \forall z.\ R(x,f(y,z)))\big)\ \land  \\
  & \big(\forall x.\ (P(x) \lor P(f(x,a)))\big)\ \land & \\
  & \big(\exists x. \forall y.\ (\neg R(x,y) \vee \neg P(y))\big)
     & \sknote{x \leadsto s_2}
\end{array}
\end{equation*}
becomes:
\begin{equation*}
\begin{array}{l@{}ll}
  & (\forall x. \ R(x,s_1(x)))\ \land
      & \sknotee{y \leadsto s_1(x)} \\
  & \big(\forall x. \forall y.\ (\neg R(x,y) \lor \forall z.\ R(x,f(y,z)))\big)\ \land  \\
  & \big(\forall x.\ (P(x) \lor P(f(x,a)))\big)\ \land & \\
  & \big(\forall y.\ (\neg R(s_2,y) \vee \neg P(y))\big)
     & \sknotee{x \leadsto s_3}
\end{array}
\end{equation*}
  
\end{frame}

\begin{frame}{Moving quantifiers and conjunctive normal form}

  Note that all bound quantified variables can be renamed while preserving equivalence and that
  quantifier can be pulled in or out of formula where it does not occur:
\begin{itemize} 
\item $(\forall x.F)  \leftrightarrow \forall y. F[x:=y]$, where $y$ is fresh
\item $(\forall x.F) \lor G \leftrightarrow \forall x.(F \lor G)$
\item $(\forall x.F) \land G \leftrightarrow \forall x.(F \land G)$
\end{itemize}
We can thus put formulas outwards. If we choose, we can obtain:
\emph{prenex normal form}, a formula of the form
\begin{equation*}
    Q_1 x_1. Q_2 x_2. \ldots Q_n x_n. G
\end{equation*}
where $Q_i \in \{\forall, \exists\}$ and $G$ has no quantifiers.

We can then transform $G$ to conjunctive normal form, as for propositional logic:
\begin{itemize} 
\item $(F \land G) \lor H \ \leftrightarrow \ (F \lor H) \land (G \lor H)$
\end{itemize}
We can also introduce fresh predicate symbols to avoid exponential blowup.
\end{frame}

\begin{frame}{Conjunction of clauses}

  Theorem: each formula $F$ can be transformed into an equisatisfiable formula
  of the form:
\begin{equation*}
    (\forall x_1,\ldots,x_n. C_1) \land \ldots \land (\forall x_1,\ldots,x_n. C_m)
\end{equation*}
where each $C_i$ is quantifier free and, moreover, a disjunction of first-order literals.

Note: a first-order literal is either an atomic formula,
that is $p(t_1,\ldots,t_k)$ where $p$ is a predicate symbol,
or a negation of an atomic formula, $\lnot
p(t_1,\ldots,t_k)$.

Indeed, we have seen how to move $\lnot$ to predicates (NNF), eliminate $\exists$, and
pull $\forall$ and $\land$ to the outside, leaving $\lor$ applied to literals.

Each $C_i$ is a (first-order) clause. We can also view it as a set, because the order of disjuncts
does not matter up to equivalence. Clause that is an empty set means $\bot$.

For a given formula $F$, denote the set of obtained clauses $\{C_1,\ldots,C_m\}$ by $clauses(F)$.

We omit universal quantifiers because all variables are universally quantified.  We use a convention to denote variables by $x,y,z,\ldots$ and constants by $a,b,c,\ldots$.

\end{frame}

\begin{frame}{Sets of formulas when checking satisfiability}
  We define that a set of formulas $S$ is true in an interpretation $I$ if \emph{every} formula
  is true in that interpretation:
  \[
  \tr{S}_I = \mbox{ if } (\forall F \in S. \tr{F}_I=1) \mbox{ then } 1 \mbox{ else } 0
  \]
  If $S$ is finite then $\tr{S}_I = \tr{\bigwedge_{F \in S} S}_I$.

  \

  We say two sets are \emph{equivalent} iff the set of
  interpretations in which they are true are equal.
  
  We say that $S$ is satisfiable iff there exists $I$ such that $\tr{S}_I = 1$.

  \
  
  Thus, $F$ is satisfiable iff $clauses(F)$ is satisfiable.
\end{frame}

\begin{frame}{Clauses for the example}
  
\begin{equation*}
\begin{array}{l@{}l}
  & (\forall x. \ R(x,s_1(x)))\ \land  \\
  & \big(\forall x. \forall y.\ (\neg R(x,y) \lor \forall z.\ R(x,f(y,z)))\big)\ \land  \\
  & \big(\forall x.\ (P(x) \lor P(f(x,a)))\big)\ \land  \\
  & \big(\forall y.\ (\neg R(s_2,y) \vee \neg P(y))\big) 
\end{array}
\end{equation*}
gives the set of clauses:
\begin{equation*}
\begin{array}{l@{}l}
\big\{ & R(x,s_1(x)),  \\
       & \neg R(x,y) \lor R(x,f(y,z)),  \\
       & P(x) \lor P(f(x,a)),  \\
       & \neg R(s_2,y) \vee \neg P(y) \big\} 
\end{array}
\end{equation*}
\pause
or, if we represent clauses themselves as sets:
\begin{equation*}
\begin{array}{l@{}l}
\big\{ & \{ R(x,s_1(x)) \},  \\
       & \{\neg R(x,y),\ R(x,f(y,z)) \},  \\
       & \{P(x), P(f(x,a))\},  \\
       & \{\neg R(s_2,y), \neg P(y)\}\ \big\} 
\end{array}
\end{equation*}

\end{frame}

\newcommand{\bx}{\overline{x}}
\newcommand{\tx}{\overline{t}}

\begin{frame}{Applying sound inference rules}

  We say that an inference rule
  \[
  \frac{F_1 \ \ldots F_n}{G} \hspace{3cm} (*)
  \]
  is \textbf{sound} iff the formula $(F_1 \land \ldots \land F_n) \rightarrow G$ is valid.

  \textbf{Observation.}
  Let $(*)$ be a sound inference rule and $F_1,\ldots,F_n \in S$. Then
  $S$ and $S \cup \{ G \}$ are equivalent.

  
  Example: using convention that variables are $\forall$ quantified, the \textbf{instantiation} rule
  \[
     \frac{C}{C[\bx:=\tx]}
   \]
   is sound, where $C[\bx:=\tx]$ denotes substituting variables of $C$ by some terms.

   In general, $\tx$ may contain other variables. Special cases of instantiation are:
   \begin{itemize}
   \item renaming: replace variables with fresh variables
   \item ground instantiation: replace variables with \emph{ground terms}, that have no variables
     (built only from constants and function symbols)
   \end{itemize}
\end{frame}

\begin{frame}{Resolution for FOL clauses}
  The following formula (transitivity of universal implication) is easily proven to be valid for all formulas $F,G,H$, where $\bx$
  denotes the finite list of all free variables in $F,G,H$:
  \[
  \big((\forall \bx.\ (F \rightarrow G)) \ \land \ (\forall \bx.\ (G \rightarrow H))\big)
  \ \ \ \rightarrow \ \ \ (\forall \bx. (F \rightarrow H))
  \]
  Write it down as an inference rule, assume that all formulas universally quantified:
  \[
  \frac{F \rightarrow G \hspace{1cm} G \rightarrow H}
       {F \rightarrow H}
  \]
  Expressing $\rightarrow$ using $\lor$ and $\lnot$:     
  \[
  \frac{\lnot F \lor G \hspace{1cm} \lnot G \lor H}
       {\lnot F \lor H}
  \]
  Let $G$ be a literal $L$, let $\lnot F$ be equivalent to clause $C_1$ and $H$ to clause $C_2$.
  We get:
  \[
  \frac{C_1 \lor L \hspace{1cm} \lnot L \lor C_2}
       {C_1 \lor C_2}
       \hspace{2cm}
       \textbf{resolution} \mbox{ (simple, without unification) }
  \]
\end{frame}

\begin{frame}{Resolution with instantiation}
  We call literals $L$ and $\lnot L$ \emph{complementary}.
  
  If literals are not complementary, we may still be able to apply substitution
  rule to make them complementary:
  \[
  \frac{{\displaystyle\frac{C'_1 \lor L'}{C_1 \lor L}} \hspace{1cm}
    {\displaystyle\frac{\lnot L'' \lor C''_2}{\lnot L \lor C_2}}}
       {C_1 \lor C_2}
  \]
  To check whether we can find a substitution to make $L'$ and $L''$ identical ($\equiv$), we
  can use (syntactic, first-order) \textbf{unification}, which has a linear-time algorithm.
  \begin{itemize}
  \item[] \wiki{Unification (computer science)}
  \end{itemize}
  We rename variables in two clauses so that they are disjoint, the instantiate them by computing
  \emph{most general unifier} computation 
  so that literals become complementary (one is an atomic formula and the other its negation).
\end{frame}

\newcommand{\sknotea}[1]{\ \ \alert{#1}}
\begin{frame}{Applying resolution}

  Apply resolution and instantiation to clauses in our example:
\begin{itemize}
\item[1] $R(x,s_1(x))$
\item[2] $\lnot R(x,y) \lor R(x,f(y,z))$
\item[3] $P(x) \lor P(f(x,a))$
\item[4] $\lnot R(s_2,y) \lor \lnot P(y)$
\item[5] \pause {\small (1,2)}: $R(x,f(s_1(x),z))$ \sknotea{$y \leadsto s_1(x)$}
\item[6] \pause {\small (1,4)}: $\lnot P(s_1(s_2))$ \sknotea{$x \leadsto s_2, y \leadsto s_1(x)$}
\item[7] \pause {\small (3,6)}: $P(f(s_1(s_2),a))$  \sknotea{$x \leadsto s_1(s_2)$}
\item[8] \pause {\small (4,7)}: $\lnot R(s_2,f(s_1(s_2),a))$ \sknotea{$y \leadsto f(s_1(s_2),a)$}
\item[9] \pause {\small (5,8)}: $\bot$ \sknotea{$x \leadsto s_2$}
\end{itemize}

\pause We can derive $\bot$ from the set of clauses.

Thus, the set of clauses is unsatisfiable. The formula we started from as well.

\end{frame}

\begin{frame}{Conclusion of the procedure on this example}
Thus, the formula before negation:
  \begin{equation*}
\begin{array}{l@{}l}
  & \big[ (\forall x. \exists y.\ R(x,y))\ \land \\
      & (\forall x. \forall y.\ R(x,y) \rightarrow \forall z.\ R(x,f(y,z)))\ \land \\
      & (\forall x.\ P(x) \lor P(f(x,a))) \big] \ \\
      & \rightarrow \forall x. \exists y.\ R(x,y) \land P(y)
\end{array}
  \end{equation*}
  was \textbf{valid}. 
  We have proven that this formula holds in all possible models (no matter how small, large, or complex
  they might be).

  \
  
  Remarkably, resolution with instantiation is
  refutationally complete: if the formula is valid, then
  from the clauses equisatisfiable to its negation we will
  find a contradiction.
\end{frame}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
