% As noted previously,
% the cut-elimination theorem of sequent calculi (which 
% says that if a sequent is provable, it is provable without using the cut rule)
% applies in all
% Display Logics, provided that the rules satisfy certain conditions, which are
% relatively easily checked (\cite{belnap-display}).
In backwards proof search, using the cut rule involves guessing
the arbitrary formula $A$; this is a disadvantage in automated proof,
as there are infinitely many choices for $A$.
The cut rule is the only rule with this property;
in all the other rules, every formula variable appearing in a premise also 
appears in the conclusion.
%Therefore, knowing that the cut rule can be avoided 
%means that, in backward proof search,
Therefore, if the cut rule can be avoided, 
then at each stage of a backward proof search 
there is only a finite number of possible next steps.
However, proofs using (cut) can often be easier to construct, and 
(cut) is necessary to make use of previously proved lemmata.

The calculus \dKt\ enjoys cut-elimination because its 
rules satisfy the conditions (C1) to (C8) 
(\cite{belnap-display,wansing-sequent}).
The construction described in this section 
eliminates the uses of (cut) from a given \dKt\ proof,
converting a proof using (cut) to one not using (cut).
This demonstrates the procedure 
used in the proof of the cut-elimination theorem.
It also allows a user to construct proofs using (cut),
knowing that a cut-free proof can be obtained \emph{automatically} if desired.

\comment{
\begin{example} \label{ex:smcut}
We give below a small example of proofs with and without (cut).
\vpf
\begin{center}
\bpf
\A "$ A \vdash A $" 
\U "$ A; B \vdash A $" "($M \vdash $)"
\U "$ (A \land B) \vdash A $" "($\land \vdash $)"

\A "$ A \vdash A $" 
\U "$ A \vdash A; C $" "($\vdash M $)"
\U "$ A \vdash (A \lor C) $" "($\vdash \lor $)"

\B [2.0em] "$ A \land B \vdash A \lor C $" "(cut)"
\epf
\hfill
\bpf
\A "$ A \vdash A $" 
\U "$ A \vdash A; C $" "($\vdash M $)"
\U "$ A \vdash A \lor C $" "($\vdash \lor $)"
\U "$ A; B \vdash A \lor C $" "($M \vdash $)"
\U "$ A \land B \vdash A \lor C $" "($\land \vdash $)"
\epf
\end{center}
\end{example}
}

The cut-elimination procedure is sketched in \cite[Appendix]{gore-relalg}.
% It may be noted that, in Example~\ref{ex:smcut},
% the cut-free proof (on the right)
% uses the same proof rules as the proof on the left (other than (cut) itself).
% Other cases involve 
% replacing a cut on a formula $A \textit{ op } B$ (say),
% together with the rules introducing the formula $A \textit{ op } B$,
% by two cuts,
% one on $A$ and one on $B$.
% Belnap's condition (C8) ensures that this can be done for each logical
% connective \textit{op}.
%
In \fig{cfk} we show the cut-free proof of the K rule
obtained by our automated cut-elimination procedure.
It has been abbreviated by combining multiple display postulate steps 
into one step labelled ``(dps)''.
Also, the automated procedure sometimes produces steps whose premise
and conclusion are the same, or a step followed by its inverse.
These have been omitted.
It will be noted that, apart from the display postulate steps, 
all the other steps used also appear in the proof in \fig{Kpf},
but many of the introduction rule steps in that proof do not appear
in the cut-free proof.
However, it is known that in general, the cut-free proof can be 
\emph{exponentially} longer than the proof from which it is constructed.

\begin{figure}[tb] %\normalsize
\begin{center}
\up 4
\begin{tabular}{c@{\hspace{-3em}}c}
\mbox{
\bpf
\A "$A \vdash A$"
\A "$B \vdash B$"
\B "$A \to B \vdash * A; B$" "($\to \vdash $)"
\U "$A \to B \vdash B; * A$" "($ \vdash P $)"
%\U "$A \to B; A \vdash B$" "((md2 ca1))"
%\U "$A \to B \vdash B; * A$" "((md1 ca1))"
\U "$\square (A \to B) \vdash \bullet (B; * A)$" "($\square \vdash $)"
\U "$\square (A \to B); \square A \vdash \bullet (B; * A)$" "($ M \vdash $)"
%\U "$\square (A \to B) \vdash \bullet (B; * A); * \square A$" "((md1 ca1))"
%\U "$\square (A \to B); \square A \vdash \bullet (B; * A)$" "((md2 ca1))"
%\U "$\square A \vdash * \square (A \to B); \bullet (B; * A)$" "((md1 ca2))"
%\U "$\square (A \to B); \square A \vdash \bullet (B; * A)$" "((md2 ca2))"
% \U "$\bullet (\square (A \to B); \square A) \vdash B; * A$" % "((md1 blob))"
% \U "$\bullet (\square (A \to B); \square A); A \vdash B$" % "((md2 ca1))"
\U "$A \vdash * \bullet (\square (A \to B); \square A); B$" "(dps)"
% "((md1 ca2))"
\U "$\square A \vdash \bullet (* \bullet (\square (A \to B); \square A); B)$"
"($\square \vdash $)"
\U "(1)"
\epf
}
&
%\hspace{-3em}
\mbox{
\bpf
\A "(1)"
\U "$\square (A \to B); \square A
\vdash \bullet (* \bullet (\square (A \to B); \square A); B)$" "($ M \vdash $)"
%\U "$\square (A \to B)
%\vdash \bullet (* \bullet (\square (A \to B); \square A); B); * \square A$"
%"((md1 ca1))"
%\U "$\square (A \to B); \square A
%\vdash \bullet (* \bullet (\square (A \to B); \square A); B)$" "((md2 ca1))"
%\U "$\square A
%\vdash * \square (A \to B); \bullet (* \bullet (\square (A \to B); \square A);
%B)$" "((md1 ca2))"
%\U "$\square (A \to B); \square A
%\vdash \bullet (* \bullet (\square (A \to B); \square A); B)$" "((md2 ca2))"
%\U "$\bullet (\square (A \to B); \square A)
%\vdash * \bullet (\square (A \to B); \square A); B$" % "((md1 blob))"
\U "$\bullet (\square (A \to B); \square A); \bullet (\square (A \to B);
\square A)
\vdash B$" "(dps)" % "((md2 ca2))"
\U "$\bullet (\square (A \to B); \square A) \vdash B$" "($ C \vdash $)"
%\U "$\bullet (\square (A \to B); \square A) \vdash B$" "((md1 seq_refl))"
%\U "$\bullet (\square (A \to B); \square A) \vdash B$" "((md2 seq_refl))"
\U "$\square (A \to B); \square A \vdash \bullet B$" "(dp)" 
% "((md1 (symmetric blob)))"
\U "$\square (A \to B); \square A \vdash \square B$" "($\vdash \square $)"
\U "$\square (A \to B) \vdash \square A \to \square B$" "($\vdash \to $)"
\U ['] "" 
\epf
}
\end{tabular}
\end{center}

\caption{Cut-Free Proof of the K rule}
\label{fig:cfk}
\end{figure}