\title{Towards a Logic for Reasoning about Logic Programs Transformation}

\author{Alberto Momigliano\thanks{ This work was mostly completed during a
visit by the first
author to the  Dipartimento di Scienze dell'Informazione, Universita'
degli studi di  Milano.} \\
Department of Philosophy \\
Carnegie Mellon University\\
15213 Pittsburgh PA, USA \\
Tel. +1-412-268-1413\\
{\tt am4e@andrew.cmu.edu}
\and
Mario Ornaghi\\
 Dipartimento di Scienze dell'Informazione\\
 Universita' degli studi di  Milano\\
 Via Comelico 39/41, Milano, Italy \\
Tel. +39-2-55006331\\
{\tt ornaghi@dsi.unimi.it}}

\date{}
\maketitle

\newcommand{\PQ}{\[ \cQ = \frac{\Pi_1}{C_1\If
\Gamma_1}{r_1},\dots,\frac{\Pi_n}{C_n \If
\Gamma_n}{r_n} \]}
\begin{abstract}
We  give a proof-theoretic analysis of logic
programs transformations,  viewed as operations on proof trees in the sense
of \cite{Hal90,Hod93,Mom94,Mom97}.  We  present a logic for reasoning about
(equivalence preserving) transformations of logic programs.
% We concentrate our analysis
% on \emph{Partial Deduction}, but we pursue also \emph{ Fold/Unfold}.
Our main tool is the usage of inference
rules; the target program may be obtained as a set of clause
introduction proofs with axioms from the source program.  The rules
are \emph{admissible}, that is every proof according to the latter  can be
translated
back in a derivation of the same consequence built from the source program
 \emph{without} those rules.
Finally, the proof-theoretic framework--we hope to show-- is much simpler
and direct than
the one based on resolution.  Moreover, it allows a uniform
generalization of the basic results  to other \lp languages satisfying
the simple requirement of \emph{regularity}.
\end{abstract}

\section{Introduction}

We  give a proof-theoretic analysis of logic
programs transformations,  viewed as operations on proof trees in the sense
of \cite{Hal90,Hod93,Mom94,Mom97}.  We  present a logic for reasoning about
(equivalence preserving) transformations of logic programs.
 Our framework is natural
deduction, although a totally analogous presentation can be given in
terms of sequent calculi with definitional reflection \cite{SH94}.
We are not
going to fully detail in this abstract the systems we are using, though we have
shown elsewhere \cite{Mom94} (and it is now beginning to be common
knowledge, see
\cite{Hod93}) that,\wrt the language of definite
clauses, interpreting $:-$ and $,$ as
implication and conjunction yields positive intuitionistic, \ie
minimal logic.  Our  basic system, let us call it $L_{0}$, contains only the
assumption rule and a rule for applying clauses ($\ap$), similar to the
rule of modus ponens.

 We shall follow this path:
\begin{enumerate}
        \item  We achieve the transformation  via the usage of inference
        rules; thus,  the target program may be obtained as a set $\cQ$ of
clause
        introduction proofs with axioms from the source program $\cP$ of the
        form:

 \PQ
        \item We show the rules to be (weakly) admissible, that is every
proof $\Pi
        :: A$ which uses those rules can be translated in a proof
        $\trad(\Pi)$ of the same consequence  \emph{without} them in the
basic system and
        axioms from $\Pi$.  As the proofs in $L_{0}$ correspond to
\SLD-derivations,
        this means that every derivation from $\cQ = C_1\If \Gamma_1,\dots,C_n
        \If \Gamma_n$ gets translated in a derivation from $\cP$.

        \item  We will look for some adequacy results. Namely,
        verifying that the success set is preserved requires certain
        completeness conditions on $\Pi_{1} ,\ldots,\Pi_{n}$;  for
        finite failure we need furthermore the \emph{strict} monotonicity
of the translation
        function.
\end{enumerate}

We pursue two applications PD and FU\ldots
 Our perspective and future aim is
the introduction of a general calculus tailored to the proof-theory of
the transformation of (logic) programs.  \medskip

The paper is organized as follows: in Section \ref{back} we review the
basic notions of our framework \cite{Mom94,Mom97} and we relate it to
\SLD-resolution \wrt success and failure.  Section (\ref{general}) presents
the  general
transformation schema. The next Section (\ref{pv}) depicts the
proof-theoretical reconstruction of Partial Deduction. Section
\ref{pt} targets Program Transformation more in general. After a
brief Conclusion


\section{Background on Proof Trees}
\label{back}
First we recall some necessary basic definitions: we assume some
familiarities with
standard notions of natural deduction \cite{Pra65} and \lp \cite{Ap90}.

We use a variant of the Axiom Application Rule introduced in
\cite{Mom94}.  We consider the \emph{Clause Application Rule} $\ap$,
for applying axioms of the form $B \If A_{1}, \dots, A_{n}$.  Using the
formalism
of natural deduction, $\ap$ can be expressed as follows:
\[
\frac{\theta A_1\cdots \theta A_n \quad\quad B \If A_1 , \dots ,
A_n}{\theta B}{\ap}
\]
where the applied clause is the {\em major premise}, $\q A_1,\dots,\q A_n$
is the (possibly empty, if $n=0$)
sequence of the {\em minor premises} and $\q B$ is the consequence.
Next, we inductively introduce the notion of {\em proof tree} (pt).

\begin{definition}[Proof Tree]
An atom $A$ is a (trivial) {\em proof tree}.  If $\Pi_1::\q A_1$,\ldots,
$\Pi_n::\q A_n$ are proof trees and $\cC$ is a clause of the form $B \If
A_1, \dots,
A_n$, then the following is also a {\em
proof tree}:
\[
{{{\displaystyle{\Pi_1\atop {\q A_{1};}}{\cdots}{\Pi_n\atop {\q
A_n;}}}\quad {\atop {\displaystyle \cC}}}\over \q B}\ap
\]

\noindent We say that, for the non-trivial case,  a formula is an {\em
assumption} of a proof tree
if it is a minor premise in some leaf.  We write this as
$$\ldots H \ldots\atop\Pi$$
The {\em clauses} of a
proof tree are the ones appearing as major premises.  The root of a
proof tree is called its {\em consequence} and is denoted by $\Pi :: B$.
  A proof tree is a {\em
proof} of $B$ from a set ${\cal P}$ of clauses iff $B$ is its
consequence, its clauses belong to ${\cal P}$ and it has no
assumption.
\end{definition}

Major premises (i.e.\  clauses) will be considered modulo renaming;
equality and substitutions on proof trees are instead defined as follows.

\begin{definition}[Proof Trees Equality]
$\Pi_{1}=\Pi_{2}$ if their major
premises   occurrences are equivalent up to renaming, while the other
 formulae occurrences are identical.
\end{definition}

\begin{definition}[Proof Trees Substitution]
$\theta \Pi$ is the tree obtained by simultaneously applying a
substitution $\theta$ to the root and to all the formulae occurring as
minor premises.  The major premises are left untouched.
\end{definition}

 The class of proof trees is closed under
% substitution \wrt the rule $\ap$.
 The subsumption ordering on formulae is then lifted to
proof trees as follows.

\begin{definition}[Subsumption Ordering]
$\Pi_{1}$ is less general than $\Pi_{2}$,
written $\Pi_{1} \leq \Pi_{2}$, if there is a substitution $\sigma$
such that $\sigma \Pi_{2}= \Pi_{1}$.  We also say that $\Pi_{2}$
subsumes $\Pi_{1}$.  Moreover, we define $\Pi_{1} \equiv \Pi_{2} \Bimp
\Pi_{1} \leq \Pi_{2} \And\Pi_{2} \leq \Pi_{1}$.
\end{definition}

One can easily see that `$\equiv$' corresponds to equivalence on proof
trees up to renaming.
 \smallskip

Now we introduce the notions of similarity and most general
proof tree.  This will allow us to abstract away from many details of
\SLD-derivations.  For example, we do not need a switching lemma or a
notion of fairness; analogously we  avoid some fastidious standardizing
apart.

 In \ref{Mom94} similarity was
defined via axiom/rule-occurrences.  For the more restricted class
of proof trees considered here, we can give a more intuitive
characterization, by means of the notion of a proof-skeleton:

\begin{definition}[Skeleton]
The \emph{Skeleton} $\sk(\Pi)$ of a proof tree $\Pi$ is defined
recursively as follows:
\begin{itemize}
\item
Basis:  $\sk(A) = []$
\item
Step:
\[
\sk\left({{{{\displaystyle{\Pi_1;\dots\Pi_n;}}\quad {\cC}}\over B}{\ap}}\right)
= {{{{\displaystyle{\sk (\Pi_1);\dots \sk (\Pi_n);}}\quad
{\cC}}\over []}{\ap}}
\]
\end{itemize}
\end{definition}
That is, the skeleton of a tree is obtained by systematically
replacing the root and minor premises with \emph{holes}: the (equivalence class
of) major premises are unchanged.

\begin{definition}[Similarity]
Two proof trees $\Pi_1$, $\Pi_2$ are  said to be {\em similar},
written $\Pi_1 \sim \Pi_2$, whenever $\sk(\Pi_1)=\sk(\Pi_2)$.
\end{definition}

One can easily see that $\sim$ is an equivalence relation.  Most
general proof trees are introduced as follows.

\begin{definition}[Most General Proof Tree]
 $\Pi$ is a {\em most general proof tree} (mgpt) if it is
{\em maximal}  among similar trees.
\end{definition}

As shown in \cite{Mom94}, the system using the rule $\ap$ is
\emph{regular}, i.e.\ for any two similar proof trees there is a
similar proof tree subsuming them.  In regular systems, each
similarity class contains a mgpt, which is unique up to renaming.
Regularity is a property also of similarity classes of
continuations of $\Pi$, i.e.\ similarity
classes containing only continuations of $\Pi$,  where
the latter are thusly defined:

\begin{definition}[Continuation]
\label{cont}
Let $ B \If A_1, \dots , A_n $ be a clause $\cC$ and
\[
{\dots \; H \dots} \atop \Pi
\]
be a proof tree with an \emph{applicable} assumption $H$, \ie such that $\q
B = \q H$, for some
substitution $\q$.  The {\em one-step continuation} of $\Pi$ {\em
selecting} $H$
and {\em applying} $\cC$ w.r.t.\ $\q$ is the proof tree:
\[
\frac{ \q A_1; \cdots ;\q A_n \qquad B \If A_1, \dots , A_n }
{{\displaystyle{\dots \; \q H \dots \atop \q\Pi}}} {\ap}\]
$\Pi_{2}$ is a \emph{continuation} of $\Pi_{1}$, written $\Pi_{1}
\preceq \Pi_{2}$, if $\Pi_{2}$ can be obtained from $\Pi_{1}$ by a
sequence of one-step continuations.
\end{definition}

Note that substitutions in continuation steps do not need to be most
general unifiers.  One can easily see that:
\begin{proposition}\label{prop:CNT}
$\Pi_{1} \preceq \Pi_{2}$
{\em if and only if\/} there is a substitution $\sigma$ such that
$\sigma \Pi_{1}$ is an initial subtree of $\Pi_{2}$.
\end{proposition}

\begin{definition}[Most General Continuations]
A continuation $\Pi^*$ of $\Pi$ is {\em most general} ({\em mgc}) if,
for every other continuation $\Delta$ similar to $\Pi^*$, $\Delta \leq
\Pi^*$.  A continuation is {\em canonical} iff it is a one-step mgc.
\end{definition}

Since similarity classes of $\Pi$-continuations are regular
\cite{Mom94}, every mgc $\Pi^{*}$ of a given $\Pi$ is unique up to
renaming.  One can also see that canonical continuations are the
one-step continuations that use most general unifiers.


\begin{definition}[Height]
The \emph{height} of a proof tree, written $h(\Pi)$, is defined here as the
length of its \emph{minimum} branch.
\end{definition}



\subsection{Proof Trees and SLD-Resolution}

Proof trees have been designed to give an exact proof-theoretical
version of \SLD-resolution: for example, let us consider the program
\emph{SUM}, containing the following clauses:
\[\begin{array}{ll}
C_0:& \quad sum(X,0,X) \If \\
C_1:& \quad sum(X,s(Y),s(Z)) \If sum(X,Y,Z) \\
\end{array}\]

An \SLD-derivation for a goal $\la \leftarrow A, \q\ra$ can be seen as a
stepwise construction of a pt $\Pi::\q A$.  Figure 1
%\ref{contfig}
shows the continuations corresponding to the
\SLD-derivation:
\[
 \begin{array}{ll}
        \leftarrow sum(ss0,s0,X_0) & \q_{1}= [X/ss0,Y/0,X_{0}/s(Z)]  \\
        \leftarrow sum(ss0,0,X_1) & \q_{2}=[Z=ss0]  \\
        \If \Box &
 \end{array}
  \]
 Notice that the formulae in the current goal correspond to the assumptions
of the relative pt.
\begin{figure}
        \label{contfig}
        \centering
\[
        \If sum(ss0,s0, X_0)    %corretto da sX
        \quad \preceq \quad
        \frac{sum(ss0,0,X_1) \quad C_1}{sum(ss0,s0,sX_1)}
        \quad \preceq \quad
         {\ova {C_0}{sum(ss0,0,ss0) \quad C_1}{sum(ss0,s0, sss0)}}
\]
        \caption{Continuations of the goal $\If sum(ss0,s0,X_0)$}
\end{figure}

In this way every \SLD-derivation can be translated into a pt and
this yields the proof-theoretical equivalence between the two systems
(see \cite{Mom94}). More formally:

\begin{definition}
A \SLD-derivation is {\em incomplete} if at any point no literal is
selected and the derivation is thusly terminated.  It is {\em relaxed}
if mgu's are not necessarily used.  If idempotent mgu's are used, then
it is {\em canonical}.

Let $P$ be a definite program, $\If G$ a goal and $\If G, \If G_1,
\dots, \If G_m$ an incomplete relaxed \SLD-derivation for $P \cup \{
\If G \}$ with substitutions $\q_1, \dots,\q_m$.  Let $\q$ be the
restriction of $\q_1 \cdots \q_m $ to the variables of $G$.  We say
that the derivation has {\em %length $m$ with computed answer $\q$ and
resultant $\q G\leftarrow G_m$}.
\end{definition}
\begin{theorem}
\label{ptequiv}
Let $P$ be a definite program and $A$ an atom:
\begin{itemize}
\item[a)]
If there is an incomplete relaxed \SLD-derivation for $P \cup \{\If
A\}$ with resultant $(\delta A \leftarrow G_m)$, then there is a
partial proof $\Pi :: \delta A$ in  $L_{0}$, using only axioms
from $P$ with open assumptions $G_m$.  If the derivation is
canonical, then $\Pi :: \delta A$ is a most general continuation of
$A$.
\item[b)]
If there is a partial proof $\Pi :: \q A$ in the $L_{0}$ with
axioms from $P$ and open assumptions $G_m$, then there is an
incomplete relaxed \SLD-derivation of $P \cup \{\leftarrow A\}$ with
resultant $(\delta A \leftarrow G_m)$.  If $\Pi :: \q A$ is a most
general continuation of $A$, then the derivation is canonical.
\end{itemize} \end{theorem}
\begin{proof}

We give the proof for $G_{0}=A$. (a)  Let $ G_0, G_1,\dots, G_m$ (with
clauses $C_1,\dots,C_m$ and substitutions $\q_1,\dots,\q_m$) be a
relaxed, possibly incomplete derivation, with $ G_0 = \:\leftarrow A$.
For $0 \leq i \leq m$, let $\delta_i$ be the composition of the
$\q_1,\dots, \q_i$ and $\leftarrow A_{i_1},\dots, A_{i_{h_i}}$ be the
atoms in the goal $ G_i$; starting with $i = 0$, we associate to $
G_0,\dots, G_i$ a proof tree $\Pi_i :: \delta_i A$ with assumptions $
A_{i_1},\dots, A_{i_{h_i}}$, as follows:

{\em Step 0}.  Associate $A$ to $ G_0$.

{\em Step i+1}.  Let $\Pi :: \, \delta_i A$ be the proof tree
associated to $ G_0,\dots, G_i$ at $step\;i$ and let $ G_{i+1}$ be
obtained applying $C_{i+1}$ to the selected atom $A_{n_i}$, with {\em
unifier} $\q_{i+1}$; build the one-step continuation of $\Pi_i :: \delta_i A$
selecting $ A_{n_i}$ and applying $C_{i+1}$ w.r.t.\ $\q_{i+1}$.
If at each step in $G_{0},\ldots, G_{n}$ we apply only mgu's, the
corresponding one-step continuations are canonical and we obtain a
mgpt.

(b)   $\Pi :: \q A$ can be obtained by at least one sequence $A = \Pi_{0}
\preceq \Pi_{1} \preceq \ldots \preceq \Pi_{n}=\Pi$; the
corresponding \SLD-derivation is $G_{0},\ldots, G_{n}$, where $G_{i}$
are the assumptions of $\Pi_{i}, i = 1\ldots n$. If $\Pi :: \q A$ is a
mgpt, then the continuations must be canonical and therefore $G_{0},\ldots,
G_{n}$ is canonical.
\end{proof}



There is a natural proof-theoretic characterization
of finite failure,
% thanks to complete sets of continuations.
\begin{definition}
An assumption is \emph{failed \wrt $\cP$} iff it has no continuation
with clauses from $\cP$. An \emph{ended
tree \wrt $\cP$} is either a proof or a proof tree with a failed assumption.
\end{definition}
\begin{definition}[Failed Proof Tree]
A proof tree $\Pi$ is {\em failed\/} with respect to a program $\cP$
if there is at least one assumption of $\Pi$ such that there are no
applicable  clause in $\cP$.
\end{definition}

\begin{proposition}[Finite Failure]
\label{ff}
An atom $A$ is finitely failed if and only if there exists a $k$ such that
 every ended pt  $\Pi :: \sigma A$ has at least one failed  assumption
 of height less or equal to $k$.
\end{proposition}

\begin{proposition}[ Failure]
\label{ff}
An atom $A$ is  failed if and only if  every ended pt  is  failed.
\end{proposition}



 You can  check that this definition of finite failure
 is equivalent to the usual one in terms of \SLD-trees and
 fairness.
`Infinite' failure is non-finite failure, \ie there is a sequence of
proof trees with increasing height. An infinite pt can be seen as the
`limit' of this sequence.
\section{The General Schema}
\label{general}


\begin{itemize}
\item[a)]
We look for (weakly) admissible rules, that allow to derive
new clauses
starting from the ones of a program $\cP$.  Weak admissibility means
that the translation $\trad$ is a partial function that is defined for all
the proofs (without assumptions) and for a suitable kind of
proof trees with assumptions.
\item[b)]
These rules
are used to transform a {\em source\/} program $\cP$ into
a {\em derived\/} program $\cQ$:
\[
\cQ = \ptuno{\Pi_1}{C_1\If \Gamma_1}{r_1},\dots,\ptuno{\Pi_n}{C_n \If
\Gamma_n}{r_n}
\]
\item[c)]
Weak admissibility entails partial correctness, i.e.\  if there is a
derivation of $A$ in $\cQ$, then there is one in $\cP$.
Completeness guarantees that the success set is preserved.
To preserve the finite failure set, completeness alone is not
sufficient, but we need also the strict monotonicity of the
translation function.
\end{itemize}

Reminder. $C_{0}$ is the (initial) calculus with the \ap rule. $C_{1}$
is the supersystem with the clause introduction rules (like \ci) of
the transformation system under scrutiny.

\begin{definition} [Weak Admissibility]
For every proof $\Pi_{1}::{\cP}\vdash_{C_{1}}H$ there is a proof
$\Pi_{0}::{\cP}\vdash_{C_{0}}H$

\end{definition}

 \begin{definition}
A set of atoms is \emph{G-closed} if each atom containing a predicate
symbol occurring in $G$ is an instance of an atom in $G$.
\end{definition}

\begin{enumerate}
\item
Partial correctness coincides with the existence of a translation
function, such that if there is a
derivation of $A$ in $\cQ$, then there is one in $\cP$.
\item
 Let $\cP$ be a source program,
 \[
 \cQ = \ptuno{\Pi_1}{A_1 \If \GG_1}{\ci} ,\dots, \ptuno{\Pi_n}{A_n \If
 \GG_n}{\ci}
  \]
 be a derived program, and $G$ be a finite set of atoms.  We say that
 $\cQ$ is \emph{$G$-complete \wrt success}  iff
 \begin{itemize}
 \item[(i)]
 For every $\Pi :: {\cP} \vdash_{L_{0}} \sigma H$, that proof can be
 partitioned as follows:
 \[
 \begin{array}{ccc}
         \Pi_{1}^{'} &\ldots  & \Pi_{n}^{'}  \\
         \delta A_{1} & \ldots & \delta A_{n}  \\
          & \Pi^{'} &   \\
          & \delta A &
 \end{array}
 \]
 \item[(ii)]
  $A_i \If \GG_i$ is \emph{G-closed}
 \end{itemize}
\item
We state  the following monotonicity properties of $\trad$ \wrt continuations:

\begin{enumerate}
%       \item
%       if $\Pi_{1} \preceq \Pi_{2}$ then $\trad(\Pi_{1}) \preceq
%       \trad(\Pi_2)$
\item
% if $\Pi_{1} \preceq \Pi_{2}$ and
$h(\Pi_{1})
        < h(\Pi_2)$ then $h(\trad(\Pi_{1})) < h(\trad(\Pi_{2}))$.
\item
if \trad \ is partial then for every pt with arbitrary high
continuations, there is a continuation $\Pi^{*}$ such that $\trad(\Pi^{*}$
is defined.
\end{enumerate}

\item
 Let $\cP,\cQ$ be as above. We say that
 $\cQ$ is \emph{$G$-complete \wrt infinite tress}  iff
 \begin{itemize}
 \item[$(i)^{'}$]
 There is a $k$ such that  every $\Pi :: {\cP} \vdash_{L_{0}} \sigma H$,
 with height$(\Pi) > k$ satisfies (i)
 \item[$(ii)^{'}$] = (ii)
 \end{itemize}

\end{enumerate}

To summarize: $\cQ$ may be
\begin{enumerate}
\item
sound (partially correct)
\item
$G$-complete \wrt success
\item
strictly monotonic
\item
$G$-complete \wrt  infinite pt's
\end{enumerate}
\begin{definition} For a program $\cP$ and a goal $G$, let $[G]$
define the closure under substitution induced by the language of $\cP$,
let $SS_{\cP}$ be the success set and $Infpt_{\cP}$ the set of infinite
pt's of $\cP$.
\end{definition}
\begin{theorem}
% \mbox{}
Given $\cP$ and $\cQ$ as above:
\begin{enumerate}
\item
entails $SS_{\cQ} \subseteq SS_{\cP}$
\item
entails $SS_{\cP}\cap [G] \subseteq SS_{\cQ} $
\item
entails $Infpt_{\cQ}\subseteq Infpt_{\cP}$
\item
entails $Infpt_{\cP}$ restricted to $[G]$ $\subseteq Infpt_{\cQ}$
\end{enumerate}
\end{theorem}
\begin{corollary}
\mbox{}

\begin{itemize}
\item[1.\ and 2.] entail success is preserved over $G$
\item[1.2.3.\ and 4.] entail success and finite failure is preserved over $G$
\end{itemize}
\end{corollary}

\section{Partial Deduction}
\label{pv}

\newcommand{\ttt}{ \prooftree \[ \[c_{0} \justifies e(0) \using \ap\]
\quad c_{2} \justifies o(s0) \using \ap \]
\quad c_{1}  \justifies e(ss0) \using \ap \endprooftree }
\newcommand{\tttt}{ \prooftree \[ \[ \ol{e(X)}^{0} \quad c_{2} \justifies
o(sX) \using \ap
\] \quad c_{1} \justifies e(ssX) \using \ap\] \justifies e(ssX) \If e(X) \using
\ci,0 \endprooftree }

We are now in the position of giving a more abstract view of
\emph{Partial Deduction} (PD) \cite{Kom93,Kom93b} thanks to our
framework.  Note that we will not be concerned with the pragmatics of
PD \cite{Sah91,PP94,DGT96} like unfolding rules, loop detection et
cetera: those issues can be treated as usual.

PD can be expressed via the converse of the clause application rule,
called clause introduction.  The rule discharges
 the ($u$-th occurrence of
the set of) assumption(s) $\GG$.
\[
\frac{{\displaystyle {\frac{\mbox{}}{\Gamma} {u}} \atop {{\displaystyle\Pi
\atop {\displaystyle C}} }}}{C \If \Gamma}{\ci,u}
\]

The latter allows the derivation of resultants. For instance,
from the program \textsl{EO}  in example \ref{oe}
we can derive the   resultant $\Pi_{0}::e(ssX) \If e(X)$:
\[
\tttt
\]
The usage of $\ap$ in
conjunction with $\ci$ yields a proof tree like the one in Figure 2.
% \ref{fi:res}.
 \begin{figure}
        \label{fi:res}
        \centering
        \[
 \prooftree \ttt \quad { \Pi_{0} \atop {e(ssX) \If e(X)}} \justifies
 e(ssss0) \using \ap \endprooftree
 \]
        \caption{Proof tree with the $\ci$ rule}
 \end{figure}


