\begin{frame}
  \frametitle{Completeness}

    A proof system is complete if it derives all formulas we want it to derive.

  
  Completeness for classical propositional logic means that
  the system derives all propositional tautologies.

  Is our example system complete with respect to formulas built from $\to$ and $0$?
  \[
  F \to (G \to F)
  \hspace*{1.5cm}
  ((F \to (G \to H)) \to ((F \to G) \to (F \to H))
  \hspace*{1.5cm}
  \frac{F \to G,F}{G}
  \]

  \

  \

  In particular, if we are given an arbitrary valid propositional
  formula (propositional tautology), is there always a way to derive it 
  using the axioms and the MP rule?

\

  \pause Does there exist a tautology that is not reachable from axioms
  using MP rule?

\

  \pause Is valid formula \ \ $0 \rightarrow a$ provable?
\end{frame}

\begin{frame}
  \frametitle{Do axioms or MP say anything about the 0 constant?}

  \[
  F \to (G \to F)
  \hspace*{1.5cm}
  ((F \to (G \to H)) \to ((F \to G) \to (F \to H))
  \hspace*{1.5cm}
  \frac{F \to G,F}{G}
  \]

  \pause No! It is as if it was any other subformula.

  Take proof
  \[\begin{array}{l}
  \ldots \\
  a \to a \\
  (a \to a) \to (0 \to (a \to a)) \ \ \ (Axiom) \\
  0 \to (a \to a) \ \ \ (MP) \\ 
  \end{array}\]

  Replace 0 with e.g. $b \to c$ in the proof above. I will get a valid proof:

  \[\begin{array}{l}
  \ldots \\
  a \to a \\
  (a \to a) \to ((b \to c) \to (a \to a)) \ \ \ (Axiom) \\
  (b \to c) \to (a \to a) \ \ \  (MP) \\ 
  \end{array}\]

  Replacing 0 with some fixed formula gives us valid proofs.
\end{frame}

\begin{frame}
  \frametitle{Our proof system cannot prove $0 \rightarrow a$}

  Suppose it can. Then it can also prove a
  formula resulting by $0$ with $a \to a$, so there would exist
  a proof of $(a \to a) \to a$.

  We have shown before that we can derive $a \to a$, so we would also derive
  $a$ using MP. 

  But $a$ is not a tautology, which is a contradiction
  with the fact that the system is sound.

  \pause

\
   
  We could add a few more axioms and get complete systems that
  were introduced by e.g. Frege and Hilbert. Instead, we will
  look at resolution as a proof system.
\end{frame}

\begin{frame}
  \huge
  \vfill
  \centerline{Towards Propositional Resolution}
  \vfill
\end{frame}


\begin{frame}
  \frametitle{A Proof System with Decision and Simplification}  

  Consider propositional formulas with $\land, \lor, \lnot$.
  
  \textbf{Case analysis proof rule.}
  $\{((F,G),F[x:=0] \lor G[x:=1]) \mid F,G \in \Formulas, 
    x - \mbox{variable} \}$:
  \[
      \frac{F \hspace{1.5cm} G}
      {F[x:=0] \lor G[x:=1]}
  \]
  Proof of soundness. To show $\{F, G\} \models (F[x:=0] \lor G[x:=1])$,
  consider an environment $e$ and assume
  $\interp{F}{e}=1$ and $\interp{G}{e}=1$. 
  \begin{itemize}
  \item  If $e(x)=0$,
  then $\interp{F[x:=0]}{e}=\interp{F}{e}=1$, so the first disjunct is $1$
  \item  If $e(x)=1$, then
  $\interp{G[x:=1]}{e}=\interp{G}{e}=1$, so the second disjunct is $1$.
  \end{itemize}
  In both cases, the disjunction evaluates to $1$ in $e$.

  \ 

  \textbf{Simplification rules} that preserve equivalence:
  $0 \land F \leadsto 0$,  $F \land 0 \leadsto 0$, \ $1 \land F \leadsto F$, $F \land 1 \leadsto F$, \ 
  $0 \lor F \leadsto F$,  $F \lor 0 \leadsto F$, \ $1 \lor F \leadsto 1$, $F \lor 1 \leadsto 1$, \ 
  $\lnot 0 \leadsto 1$, \ $\lnot 1 \leadsto 0$. 

  Introduce inferences $\{((F),F') \mid F' \mbox{ is simplified } F\}$.
  These rules are also sound. Call this $\InferDec$.
\end{frame}

\begin{frame}
  \frametitle{Example Derivation}
  Derivation from $A = \{ a \land b, \ \lnot b \lor \lnot a\}$. Draw the arrows to get a proof DAG

  \ 

  \fbox{$a \land b$}  \hspace*{4cm}  \fbox{$\lnot b \lor \lnot a$}

   \

  \begin{minipage}{3cm}
  \hspace{2cm} \fbox{$(0 \land b) \lor (1 \land b)$}

  \ 

  \hspace{2.5cm} \fbox{$b$}  
  \end{minipage}
  \begin{minipage}{3cm}  
  \hspace{2cm}  \fbox{$(a \land 0) \lor (a \land 1)$}

  \ 

  \hspace{2.5cm} \fbox{$a$}
  \end{minipage}

  \ 

  \hspace{4cm}\fbox{$0 \lor (\lnot 1 \lor \lnot a)$}

  \

  \hspace{1.5cm}\fbox{$\lnot a$}

  \hspace{2cm}\fbox{$0 \lor (\lnot 1)$}

  \hspace{3cm}\fbox{$0$}


  \pause
  This derivation shows that: $A \vdash 0$
\end{frame}

\begin{frame}
  \frametitle{Proving Unsatisfiability}

  A \emph{set} $A$ of formulas is \emph{satisfiable} if there exists
  $e$ such that, for every $F \in A$, $\interp{F}{e}=1$.
  \begin{itemize}
    \item when $A = \{F_1,\ldots,F_n\}$ the notion is the same as 
        the satisfiability of $F_1 \land \ldots \land F_n$
  \end{itemize}
  Otherwise, we call the set $A$ \emph{unsatisfiable}.

  \begin{theorem}[Soundness Consequence]
    If $A \vdash_{\InferDec} 0$ then $A$ is unsatisfiable.
  \end{theorem}
  If there exists $e$ is such that $e(F)=1$ for all $F \in A$ then
  by soundness of $\InferDec$, $e(0)=1$, a contradiction. So there is no such $e$.

  \begin{theorem}[Refutation Completeness]
    If a finite set $A$ is unsatisfiable, then
    $A \vdash_{\InferDec} 0$
  \end{theorem}
  
  Proof hint: take conjunction of formulas in $A$ and existentially quantify it to get $A'$. What is the relationship
  of the truth of $A'$ and the satisfiability of $A$? 
  For a conjunction of formulas $F$, can you express $\exists x. F$ using $\InferDec$?
\end{frame}

\begin{frame}
  \frametitle{Illustration of Completeness}

   Let $A = \{F_1,F_2\}$ and let $FV(F_1) \cup FV(F_2) = \{x_1,\ldots,x_n\}$ and let $x$ be some $x_i$

   We have the following equivalences:
   \[\begin{array}{cc}
     \exists x. (F_1 \land F_2) \\
     (F_1 \land F_2)[x:= 0] \lor (F_1 \land F_2)[x:=1]  & \mbox{try both values} \\
     (F_1[x:=0] \land F_2[x:= 0]) \lor (F_1[x:=1] \land F_2[x:= 1]) & \mbox{meaning of substitution} \\
     (F_1[x:=0] \lor F_1[x:=1]) \land 
     (F_1[x:=0] \lor F_2[x:=1]) \land  \\
     (F_2[x:=0] \lor F_1[x:=1]) \land 
     (F_2[x:=0] \lor F_2[x:=1])
   \end{array}\]
   Existentially quantifying over a variable gives us result of applying decision rule to all pairs of formulas $F_1,F_2$.

   Systematically applying rules will derive formula $Z$ equivalent to $\exists x_1.  \ldots \exists x_n. (F_1 \land F_2)$.

   When $A$ is unsatisfiable, $Z$ is equivalent to 0, and has no free variables. By simplification rules, we can derive $0$.
\end{frame}

\begin{frame}
  \huge
  \vfill
  \centerline{Resolution on Clauses}
  \vfill
\end{frame}

\begin{frame}
  \frametitle{Conjunctive Form, Literals, and Clauses}

  A propositional \emph{literal} is either a variable (e.g., $x$) or its negation ($\lnot x$).
  
  A \emph{clause} is a disjunction of literals. 
  
  For convenience, we can represent clause as a finite \emph{set of literals} \\
  (because of associativity, commutativity, and idempotence of $\lor$).

  \ 

  Example: $a \lor \lnot b \lor c$ represented as $\{a, \lnot b, c\}$

  \ 

  If $C$ is a clause then $\interp{C}{e}=1$ iff there exists a literal $L \in C$
  such that $\interp{L}{e}=1$.

  We represent $0$ using the empty clause $\emptyset$.

  As for any formulas, a finite set of clauses $A$ can be interpreted as a conjunction.

  Thus, a set of clauses can be viewed as a formula in conjunctive normal form:
  \[
       A = \{ \{a\},\ \{b\},\ \{\lnot a, \lnot b\} \}  
  \]
  represents the formula
  \[
       a \land b \land (\lnot a \lor \lnot b)
  \]
\end{frame}

\begin{frame}
  \frametitle{Resolution on Clauses as a Proof System}

  \begin{tabular}{c|c}
  \begin{minipage}{6cm} \centering
  \fbox{$a \lor b \lor c$} \hspace{2cm} \fbox{$d \lor \lnot c$}  \\
  \fbox{$(a \lor b \lor 0) \lor (d \lor \lnot 1))$} \\
  \fbox{$a \lor b \lor d$}
  \end{minipage} &
  \begin{minipage}{6cm} \centering
  \fbox{$\{a,b,c\}$} \hspace{2cm} \fbox{$\{d,\lnot c\}$} \\
  \ \\ \ \\
  \fbox{$\{a,b,d\}$}
  \end{minipage}

  \end{tabular}
  
  \ 

  Clausal resolution rule (decision rule for clauses):
  \[
      \frac{C_1 \cup \{x\} \ \ \ C_2 \cup \{\lnot x\}}
           {C_1 \cup C_2}
           \hspace*{2cm}{\mbox{resolve two clauses with respect to $x$}}
  \]
  \begin{theorem}[Soundness]
    Clausal resolution is sound: for all clauses $C_1,C_2$ and propositional variable $x$, 
    $\{C_1 \cup \{x\}, C_2 \cup \{\lnot x\}\} \models C_1 \cup C_2$.
  \end{theorem}
  \begin{theorem}[Refutational Completeness]
    A finite set of clauses $A$ is unsatisfiable if and only if there exists a derivation
    of the empty clause from $A$ using clausal resolution.
  \end{theorem}
\end{frame}

\begin{frame}
  \frametitle{Resolution as Transitivity of Implication}

  For three formulas $F_1,F_2,F_3$ if $F_1 \rightarrow F_2$ and $F_2 \rightarrow F_3$ are true, so is $F_1 \to F_3$.

  Thus, $\rightarrow$ denotes a transitive relation on $\{0,1\}$.

  \

  We can view resolution as a consequence of transitivity.

  We use the fact that $P \rightarrow Q$ is equivalent to $\lnot P \lor Q$:

  \begin{tabular}{cc}
  \begin{minipage}{4cm}
  \[
      \frac{C_1 \lor x \ \ \ C_2 \lor \lnot x}
           {C_1 \lor C_2}
  \]
  \end{minipage}
  \begin{minipage}{4cm}
    \[
        \frac{(\lnot C_1) \rightarrow x \ \ \ x \rightarrow C_2}
             {(\lnot C_1) \rightarrow C_2}
    \]
    \end{minipage}
  \end{tabular}

\end{frame}

\begin{frame}
  \frametitle{Exercise}
  Use resolution to prove that the following formula is valid:
  \[
      \lnot (a \land b \land (\lnot a \lor \lnot b))
  \]
  
  \pause
  Prove that its negation is unsatisfiable set of clauses:
  \begin{minipage}{7cm}
  \[
     \{a\} \hspace{1cm} \{b\} \hspace{1cm} \{\lnot a, \lnot b\}
  \]
  \pause
  \[
      \{\lnot b\}
  \]
  \pause
  \hspace{2cm}
  $
      \emptyset
  $
  \end{minipage}

\end{frame}

\begin{frame}
  \frametitle{Unit Resolution}

  A \emph{unit clause} is a clause that has precisely one literal; it's of the form $\{L\}$

  Given a literal $L$, its complement $\bar L$ is defined by $\overline x = \lnot x$, \ \ $\overline {\lnot x} = x$.

  \ 

  Unit resolution is a special case of resolution where at least one of the clauses is a unit clause:
  \[
      \frac{C \hspace{1cm} \{L\}}
           {C \setminus \{\overline L\}}
  \]
  Soundness: if $L$ is true, then $\overline L$ is false, so it can be deleted from a disjunction $C$.

  \ 

  Subsumption: when applying resolution, if we obtain a clause $C' \subseteq C$ that is subset of a previosly derived one, we
  can delete $C$ so we do not consider it any more. Any use of $C$ can be replaced by use of $C'$ with progress towards $\emptyset$
  at least as good.

  \ 
  
  If we derive $\{L\}$ we can remove all other occurrences of $L$ and $\overline L$:
  if $L \in C$ then $C$ is subsumed by $\{L\}$ and if $\bar L \in C$ then $C$ is
  subsumed by $C \setminus \{\overline L\}$.
\end{frame}

\begin{frame}
  \huge
  \vfill
  \centerline{From Formulas to Clauses}
  \vfill
\end{frame}

\begin{frame}
  \frametitle{Constructing a Conjunctive Normal Form}

  How would we transform this formula into a set of clauses:
  \[
      \lnot \left( 
               ((c \land a) \lor (\lnot c \land b)) \leftrightarrow
               ((c \rightarrow b) \land (\lnot c \rightarrow b))
           \right)
  \]
  Which equivalences are guaranteed to produce a conjunctive normal form?
  \[\begin{array}{rcl}
      \lnot (F_1 \land F_2) &\leftrightarrow& (\lnot F_1) \lor (\lnot F_2)  \\
      F_1 \land (F_2 \lor F_3) &\leftrightarrow& (F_1 \land F_2) \lor (F_1 \land F_3) \\
      F_1 \lor (F_2 \land F_3) &\leftrightarrow& (F_1 \lor F_2) \land (F_1 \lor F_3) \\
  \end{array}\]
  \pause
  What is the complexity of such transformation in the general case?

  \pause
  Are there efficient algorithms for checking satisfiability of formulas in \emph{disjunctive} normal form
  (disjunctions of conjunctions of literals)?

  When checking satisfiability, is conversion into \emph{conjunctive} normal form any better
  than disjunctive normal form?
\end{frame}

\begin{frame}
  \frametitle{Discussion of Normal Form Transformation}

  Transformation is exponential in general, applying from left to right equivalence 
  \[
     F_1 \lor (F_2 \land F_3) \leftrightarrow (F_1 \lor F_2) \land (F_1 \lor F_3) 
  \]
  duplicates sub-formulas $F_1$, which may result in an exponentially larger formula.

  \ 

  If we were willing to do transformation using those rules, we might just as well transform formula
  into \emph{disjunctive} normal form, because checking satisfiability of formula in disjunctive normal
  form is trivial, such formula is a disjunction of conjunctions $D_i$ and we have these equivalences:
  \[\begin{array}{c}
    \exists e. \interp{D_1 \lor \ldots \lor D_n}{e}=1 \\
    \exists e. (\interp{D_1}{e}=1 \lor \ldots \lor \interp{D_n}{e}=1) \\
    (\exists e. \interp{D_1}{e}=1) \lor \ldots \lor (\exists e. \interp{D_n}{e}=1) \\   
  \end{array}\]
  and the last condition is trivial to check, because we check satisfiability of conjunction $D_i$
  separately.
\end{frame}


\begin{frame}
  \frametitle{Equivalence and Equisatisfiability}

  Formulas $F_1$ and $F_2$ are \textbf{equivalent} iff: $F_1 \models F_2$ and $F_2 \models F_1$
  ($\forall e. \interp{F_1}{e}=\interp{F_2}{e}$)

  \ \\

  Formulas $F_1$ and $F_2$ are \textbf{equisatisfiable} iff: $F_1$ is satisfiable whenever $F_2$
  is satisfiable.

  \ \\

  Equivalent formulas are always equisatisfiable, but the converse is not the case in general.
  For example, formulas $a$ and $b$ are equisatisfiable, because they are both satisfiable.

  \ \\

  Consider these two formulas:
  \begin{itemize}
    \item $F_1$: \ \ $(a \land b) \lor c$
    \item $F_2$: \ \ $(x \leftrightarrow (a \land b)) \ \land\ (x \lor c)$
  \end{itemize}
  They are equisatisfiable but not equivalent. For example, given $e = \{(a,1),(b,1),(c,0),(x,0)\}$,
  $\interp{F_1}{e}=1$ whereas $\interp{F_2}{e}=0$. Interestingly, every choice of $a,b,c$ that makes $F_1$ true can be 
  extended to make $F_2$ true appropriately, if we choose $x$ as $\interp{a \land b}{e}$.
\end{frame}


\begin{frame}
  \frametitle{Flatenning as Satisfiability Preserving Transformation}

  Observation: Let $F$ be a formula, $G$ another formula, and $x \notin FV(F)$ a propositional variable. 
  Let $F[G:=x]$ denote the result of replacing an occurence of formula $G$ inside $F$ with $x$.
  Then $F$ is equisatisfiable with 
  \[ 
      (x = G) \land F[G:=x]
  \]
  (Here, $=$ denotes $\leftrightarrow$.)

  Proof of equisatisfiability: a satisfying assignment for new formula is also a satisfying assignment for the old one.
  Conversely, since $x$ does not occur in $F$, if $\interp{F}{e}=1$, we can change $e(x)$ to
  be defined as $\interp{G}{e}$, which will make the new formula true.

  \ 

  (A transformation that produces an equivalent formula: \emph{equivalence preserving}.)

  A transformation that produces an equisatisfiable formula: \emph{satisfiability preserving}.

  Flattening is this satisfiability preserving transformation in any formalism that supports equality (here: equivalence):
  pick a subformula and given it a name by a fresh variable, applying the above observation.

  Strategy: apply transformation from smallest non-variable subformulas.
\end{frame}

\begin{frame}
  \frametitle{Tseytin's Transformation (see also Calculus of Computation, Section 1.7.3)}

  Consider formula with $\lnot,\land,\lor,\rightarrow,{=},\oplus$

  \begin{itemize}
  \item Replace $F_1 \rightarrow F_2$ with $\lnot F_1 \lor F_2$ and push negation into the propositional 
  variables using De Morgan's laws and switching between $\oplus$ and $=$.
  \item Repeat: flatten an occurrence of a binary connective whose arguments are literals
  \item In the resulting conjunction, express each equivalence as a conjunction of clauses:
  \end{itemize}
  \[\begin{array}{rcl|l}
    \multicolumn{3}{c|}{\mbox{conjunct}} & \mbox{corresponding clauses} \mnl
     x &=& (a \land b)  & \{\overline{x},a\}, \{\overline{x},b\}, \{\overline{a}, \overline{b}, x\}  \mnl
     x &=& (a \lor b)   & \{\overline{x}, a, b\}, \{\overline{a}, x\}, \{\overline{b}, x\}  \mnl
     x &=& (a = b) & \mnl
     x &=& (a \oplus b) & 
  \end{array}\]
  Exercise: Complete the missing entries. 
  Are the rules in the last step equivalence preserving or only equisatisfiability preserving?
  Why is the resulting algorithm polynomial?
\end{frame}

\begin{frame}
  \frametitle{Example: Find an Equisatisfiable Set of Formulas in CNF}
  \[\begin{array}{l}
    \{ \fbox{$c \land a$} \lor (\lnot c \land b) \} \mnl
    \pause
    \{x_1 \lor \fbox{$\lnot c \land b$}, \ x_1 \leftrightarrow (c \land a) \} \mnl
    \pause
    \{x_1 \lor x_2, \begin{array}[t]{l} 
                        x_2 \leftrightarrow (\lnot c \land b), \\ 
                        x_1 \leftrightarrow (c \land a) \} \mnl
                    \end{array} \mnl
    \pause
    \{x_1 \lor x_2, \begin{array}[t]{l} 
                      x_2 \rightarrow (\lnot c \land b),\ (\lnot c \land b) \rightarrow x_2, \\ 
                      x_1 \rightarrow (c \land a),\ (c \land a) \rightarrow x_1 \} \mnl
                      \end{array} \mnl
    \{x_1 \lor x_2, \begin{array}[t]{l} 
                        \lnot x_2 \lor \lnot c,\ \lnot x_2 \lor b,\ c \lor \lnot b \lor x_2, \\ 
                        \lnot x_1 \lor c,\ \lnot x_1 \lor a,\ \lnot c \lor \lnot a \lor x_1 \}
                        \end{array} 
    \end{array}\]
   When representing clauses as sets:
   \[
    \{\{x_1, x_2\}, \begin{array}[t]{l} 
      \{\lnot x_2, \lnot c \},\ \{\lnot x_2, b\},\ \{c , \lnot b, x_2\}, \\ 
      \{\lnot x_1, c\},\ \{\lnot x_1, a\},\ \{\lnot c, \lnot a, x_1\} \}
      \end{array} 
\]    
  \vspace*{6cm}
\end{frame}

\begin{frame}
  \huge
  \vfill
  \centerline{Finding Proofs}
  \vfill
\end{frame}

\begin{frame}
  \frametitle{SAT Solvers}

  A SAT solver takes as input a set of clauses.

  \ 

  To check satisfiability, convert to equisatisfiable set of clauses in polynomial time using Tseytin's transformation.

  \ 

  To check validity of a formula, take negation, check satisfiability, then negate the answer. 

  \ 

  How should we check satisfiability of a set of clauses?
  \begin{itemize}
    \item resolution on clauses, favoring unit resolution and applying subsumption (complete) \\
       Davis and Putnam, 1960
    \item truth table method: check one value of a variable, then other (space efficient)
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Davis-Putnam-Logemann-Loveland (DPLL) Algorithm Sketch}

  \lstinputlisting[language=pscala]{DPLL.scala}
\end{frame}

\begin{frame}
  \frametitle{Data Structures in a SAT Solver}

   Previous algorithm 
   \begin{itemize}
    \item generates new clauses in \lstinline|UnitProp|
    \item deletes clauses in \lstinline|UnitProp| and \lstinline|subsumption|
   \end{itemize}
   This is very inefficient. SAT solvers use more efficient data structures:
   \begin{itemize}
    \item all unit clauses are represented as a current assignment: a \emph{partial map}, environment $e$
      from some of the variables to truth values (starts as empty map)
      \begin{itemize}
        \item unit clause $\{\lnot a\}$ becomes $e(a)=0$, unit clause $\{a\}$ becomes $e(a)=1$
      \end{itemize}
    \item whenever a new literal $L$ becomes true, we check if $e$ assigns its value in the contradictory way
          and, if so, we detect a \emph{conflict}, corresponding to $\emptyset$
    \item instead of resolving $\{L_1,L_2,\ldots,L_n\}$ with a unit literal $\{\overline{L_1}\}$: interpret each
         clause in the context of current $e$: once $\interp{L_1}{e}=0$, we interpret clause as $\{L_2,\ldots,L_n\}$
    \item when all literals in a clause are $0$ except for one literal, say, a variable $p$, then $p$ must be true,
      so update assignment $e' = e \cup \{(a, 1)\}$, but report contradiction if already $e(a)=0$.
      \emph{Two-watched literal} data structure makes detecting this fast.
    \item instead of subsumption: mark and ignore clauses that are true in current $e$
    \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Clause Learning. Generating Proofs from SAT Solver Runs}

  CDCL (conflict-driven clause learning): the solver maintains the progress in exploring the space
  using learned clauses.
  Each learned clause is derived by resolution from existing ones. For example, if decisions that set literals
  $L_1,L_2,L_3$ to true lead to a conflict, then the clause $\lnot (L_1 \land L_2 \land L_3)$ is a resolution consequence
  of the input formula, so we can add it to a clause set.

  \ 

  Given the length of proofs and subtlety of SAT solvers, there exist very compact formats (e.g. DRAT) that can be 
  checked independenty using simple and efficient proof checkers, which operate in polynomial time.

  \ 

  There exists combinatorial statements (e.g. Pigenhole principle) that generate an infinite family of
  unsat formulas $F_1, F_2, \ldots$ such that the shortest \emph{resolution} proof $F_i \vdash \emptyset$ is exponential
  in the size of $F_i$ (Urquhart 1987).
    No such hard cases are known for \emph{extended} resolution, which can introduce fresh propositional variables
  that name given clauses (Audemard, Katsirelos, Simon, AAAI-10). An efficiently checkable proof system with short proofs would imply NP = coNP.
\end{frame}
