draft.tex

\documentclass{article}

\usepackage[utf8x]{inputenc}

\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{xcolor}
\usepackage{hyperref}
\usepackage{bussproofs}

\usepackage{listings}

\input{DIALEKTO}

\newcommand{\Term}{\text{Term}}
\newcommand{\Formula}{\text{Formula}}
\newcommand{\schem}[1]{{'\hspace{-0.2em}#1}}

\title{Sequent calculus style in Dedukti}
\author{Simon Guilloud and Amélie Ledein}
\date{}

\begin{document}

	\maketitle

	\begin{abstract}
		This draft presents a sequent calculus in Dedukti in order to translate and recheck LISA proofs in the future.
	\end{abstract}

	Computer science is spreading increasingly in everyday human life: medecine, transport, communication or also teaching. In some circumstances, software is the critical part of a process as human lives are at stake.
	For that reason, research at the intersection between mathematics, computer science and logic develops various formal tools
	% Formal tools exist and are based on different logics.
	based on different logics to increase the confidence over softwares.
	Such tools can be SAT or SMT solvers, 
	%proof assistants as 
	Lean, Coq, Agda, B, HOL Light, Isabelle, PVS, Metamath, K, etc.
	To deeply study and understand the logical differences between all these formal tools, some logical frameworks have been elaborated such as Dedukti.

	Dedukti is a logical framework based on the $\lambda\Pi$-calculus modulo theory, a typed $\lambda$-calculus with dependent types and rewriting rules.
	Various features and logics have been already defined such as Calculus of Construction~\ref{}, universe polymorphism~\ref{}, predicate subtyping~\ref{}, etc.
	The flexibility and the expressivity of this logical framework suggest that Dedukti is a good candidate to allow interoperability of proofs.
	However logics based on sequent calculus are less explored. \\


	%\begin{itemize}
	%	\item justification de Dedukti
	%	\item contribution
	%\end{itemize}

	After presenting Dedukti as well as sequent calculus, this article proposes an encoding of sequent calculus 

\newpage

	\section{Preliminaries}

	This section introduces the logical framework Dedukti (\autoref{SSect:Dedukti}), the first-order logic (\autoref{SSect:FOL})

	higher-order abstract syntax (\autoref{SSect:HOAS})

	Sequent Calculus (\autoref{SSect:sequent-calculus}).

	\subsection{Dedukti}\label{SSect:Dedukti}
	
	Dedukti is a logical framework inspired from LF one.
	
	A theory in Dedukti is a set of symbols and a set of rewriting rules.
	
	using dependent types, Curry-De Bruijn-Howard isomorphism and rewriting rules.
	

	
	
	Now we can define natural numbers.
	
	% Natural numbers
	\lstinputlisting[language=Dialekto, firstnumber=last, linerange={20-20, 22-23}]{SimpleVersion/prelude.lp}
	
	This declaration is very similar to the definition of an inductive type.
	
	
	To define polymorphic lists
	As the declaration \lstinline[language=Dialekto, firstnumber=last]|constant symbol List: TYPE → TYPE;| is ill-formed since  a symbol with an  type.
	
	
	Thanks to rewriting rules, it is possible to leave the rewriting engine of Dedukti to do computations.
	
	To be able to do polymorphism, we need to declare the type \textsf{Set}.
	
	\lstinputlisting[language=Dialekto, firstnumber=last, linerange={1-1}]{SimpleVersion/prelude.lp}
	
	and a mapping from \textsf{Set} to TYPE.
	
	Interpretation of set codes in TYPE
	
	\lstinputlisting[language=Dialekto, firstnumber=last, linerange={5-5}]{SimpleVersion/prelude.lp}
	
	

	
	
	
	
	
	%List
	\lstinputlisting[language=Dialekto, firstnumber=last, linerange={7-9,11-11}]{SimpleVersion/prelude.lp}
	
	In order to be able to declare lists over natural numbers, we need to define a type of natural numbers at the level of \textsf{Set} and map it to the one at the level of \lstinline[language=Dialekto, firstnumber=last]|TYPE| thanks to a rewriting rule.
	
	\lstinputlisting[language=Dialekto, firstnumber=last, linerange={29-29,31-31}]{SimpleVersion/prelude.lp}
	
	
	Thanks to rewriting rules, Dedukti allows us to define functions to compute.
	For instance, the following rewriting rules associated to the symbol \textsf{append} compute the concatenation of two lists.
	The definition is similar to a pattern-matching declaration over the first argument.
	
	% Append
	\lstinputlisting[language=Dialekto, firstnumber=last, linerange={13-13,15-16}]{SimpleVersion/prelude.lp}
	
	\noindent Thanks to the induction principle over lists, it is possible to prove that \lstinline[language=Dialekto, firstnumber=last]|Π Γ, append Γ Nil = Γ|.
	
	\lstinputlisting[language=Dialekto, firstnumber=last, linerange={17-17}]{SimpleVersion/prelude.lp}
	
	% Map and reverse -- Pas utilisé
	%   the symbol \textsf{map}
	%   the symbol \textsf{reverse}
	%\lstinputlisting[language=Dialekto, firstnumber=last, linerange={33-39}]{SimpleVersion/prelude.lp}
	
	\noindent Following the same idea, we can declare the polymorphic function \textsf{swap} $l$ $n$, which swaps the $n$-th argument of the list $l$ with the ($n+1$)-th one.
	
	\lstinputlisting[language=Dialekto, firstnumber=last, linerange={104-108}]{SimpleVersion/prelude.lp}
	
	
	We have just presented the basic concepts in order to encode a logic into Dedukti. Now we are ready to remain first-order logic and present a encoding of FOL in Dedukti.
	
\newpage

	A formula respects the following grammar where $t ::= x~|~...~~$: \\
	$\phi ::= \textsf{Top}~|~\textsf{Bot}~|~\phi~\land~\phi~|~\phi~\lor~\phi~|~\phi~\textsf{Implies}~\phi~|~\textsf{Forall}~f~|~\textsf{Exists}~f~|~\textsf{Neg}~\phi~|~\phi~\textsf{Iff}~\phi~|~\textsf{ExistsUniq}~f~|~t~\textsf{Equality}~t$
	
	\lstinputlisting[language=Dialekto, firstnumber=last, linerange={13-14,16-18,20-21,23-25}]{SimpleVersion/FOL.lp}
	
	\lstinputlisting[language=Dialekto, firstnumber=last, linerange={11-11}]{SimpleVersion/FOL.lp}
	
	The combinaison of these symbols defines formulas.
	In order to do proofs, .
	
	\begin{lstlisting}[language=Dialekto, firstnumber=last]
symbol fprf : Formula → TYPE;
	\end{lstlisting}
	
	\begin{lstlisting}[language=Dialekto, firstnumber=last]
symbol id-ax A : fprf (A Implies A);
symbol iff-ax A B : fprf (A Implies B) → fprf (B Implies A) → fprf (A Iff B);
	\end{lstlisting}
	
	
	\begin{lstlisting}[language=Dialekto, firstnumber=last]
symbol equiv-prf A : fprf (A Iff A) := iff-ax A A (id-^ax A) (id-ax A);
	\end{lstlisting}

\newpage	
	
	\subsection{First-Order Logic with Equality and Schematic Variables}\label{SSect:FOL}
	We consider first-order logic with logical operators $(\neg, \land, \lor, \rightarrow, \leftrightarrow, \forall, \exists, \exists !)$, where $\exists !$ denotes the unique existential. We also consider $=$ as a built-in equality symbol, and accept schematic function and predicate symbols. A schematic symbol is a second-order variable that cannot be bound. It can be substituted, but behaves otherwise like an uninterpreted function or predicate symbol.
	
	We define the types of \textit{terms} and \textit{formulas}:

	\begin{lstlisting}[language=Dialekto, firstnumber=last]
constant symbol Term : TYPE;
constant symbol Formula : TYPE;
	\end{lstlisting}
	Our encoding imposes no requirements on the structure of terms. In practice,  for every function symbol $f$ of arity $n$ in the source language, the user needs to define a corresponding symbol:
	\begin{lstlisting}[language=Dialekto, firstnumber=last]
constant symbol f :  Term → ... → Term
	\end{lstlisting}
	and similarly for predicate symbols
	\begin{lstlisting}[language=Dialekto, firstnumber=last]
constant symbol p :  Term → ... → Formula
	\end{lstlisting}
	As we consider first order logic with equality and have special rules for it, we define the equality symbol:
	\begin{lstlisting}[language=Dialekto, firstnumber=last]
constant symbol Equality :  Term → Term → Formula
	\end{lstlisting}
	We also define the boolean operators:
	\begin{lstlisting}[language=Dialekto, firstnumber=last]
symbol Neg : Formula → Formula;
symbol ∧ : Formula → Formula → Formula; notation ∧ infix right 30;
symbol ∨ : Formula → Formula → Formula; notation ∨ infix right 30;
symbol Implies : Formula → Formula → Formula;
symbol Iff : Formula → Formula → Formula;
\end{lstlisting}
%symbol Forall : (Term → Formula) → Formula;
%symbol Exists : (Term → Formula) → Formula;
%symbol ExistsOne : (Term → Formula) → Formula;
%	\end{lstlisting}
	\subsection{Higher-Order Abstract Syntax}\label{SSect:HOAS}
	Higher-Order Abstract Syntax (HOAS) is an approach to make shallow encoding of a system (in our case FOL) in an other (Dedukti) where variables of the original are represented as variable of the target system and not as syntactic objects. As it is not possible to express globally free variables in Dedukti, a formula with a free variable is encoded the following way:
	$$
	P(x_1) \land Q(x_1) \rightsquigarrow \lambda x_1 ,  P(x_1) \land Q(x_1)
	$$
	Note that the term on the right has type $\Term \rightarrow \Formula$. We then want
	$$
	\forall x_1, P(x_1) \land Q(x_1) \rightsquigarrow \forall (\lambda x_1 ,  P(x_1) \land Q(x_1))
	$$
	so that the universal quantifier $\forall$ is an operator with type \lstinline[language=Dialekto, firstnumber=last]|(Term → Formula) → Formula|, and similarly for $\exists$ and $\exists !$. In Dedukti, we hence define:
	\begin{lstlisting}[language=Dialekto, firstnumber=last]
symbol Forall : (Term → Formula) → Formula;
symbol Exists : (Term → Formula) → Formula;
symbol ExistsOne : (Term → Formula) → Formula;
\end{lstlisting}
%	\end{lstlisting}
This type of encoding automatically takes care of, for example, capture-avoiding substitutions. Schematic symbols can be represented the same way. Consider for example the following fixed point statement:
$$
	(\forall x, 'P(x) \rightarrow 'P(f(x))) \rightarrow (\forall x, 'P(x) \rightarrow 'P(f(f(x))))
$$
It holds for any particular substitution of $'P$ by a formula and $'f$ by a term. This is naturally represented in Dedukti by using abstracting over $'P$ and $'f$ with $\lambda 'P, 'f: (\forall x, ('P x) \rightarrow ('P(f x))) \rightarrow (\forall x, ('P x) \rightarrow ('P (f (f x))))$.
	
	+ $\forall$ binds (higher-order abstract syntax: $\forall x.~A$ expressed as $\forall~\lambda x.~A$)
	
	\iffalse
	We consider first order logic with arbitrary constant function and predicate symbols. Fomally We fix:
	\begin{itemize}
		\item a set of constant symbols $C$ noted $f^j, g^j, h^j, f^j_i,...$ for indices $i\in \mathbb{N}$ and where the superscript $j$ denotes the \textit{arity} of the symbol
		\item a countably infinite set of schematic function symbols $'C$ noted $ 'f^j, 'g^j, 'h^j, f^j_i,...$ for indices $i\in \mathbb{N}$ and where the superscript $j$ denotes the \textit{arity} of the symbol.
	\end{itemize}
	We also call schematic functions symbols of arity 0 \textit{variables}, and note them $x,y,z$.
	The set of terms of height at most $n$ is
	$$\mathcal{T}_0 := \lbrace f^0 \mid f^0 \in C\rbrace \cup \lbrace 'f^0 \mid 'f^0 \in C \rbrace$$
	$$\mathcal{T}_{n+1} := \mathcal{T}_n \cup \lbrace f^j(\vec{t}) \mid f^j\in \mathcal{C}, \vec{t}\in \mathcal{T}_n^j, j>0 \rbrace \cup \lbrace 'f^j(\vec{t}) \mid 'f^j\in \mathcal{C}, \vec{t}\in \mathcal{T}_n^j, j>0 \rbrace$$
	and the set of all termsis $\mathcal T = \bigcup_{n=0}^\infty \mathcal{T}_n$.  Moreover, we allow \textit{schematic functions, predicate and connector symbols}.
	
	\fi

	\subsection{Sequent calculus}\label{SSect:sequent-calculus}
	The Sequent Calculus LK is a proof system for first-order logic. A \textit{sequent} is a pair of ordered lists of formulas, noted
	$$
	\Gamma \vdash \Delta
	$$
	We usually use capital greek letter to denote sets of formulas. In an expression such as $\Gamma, \Sigma \vdash \phi, \Delta$, the comma denotes concatenation. In Dedukti, a sequent is:
	\begin{lstlisting}[language=Dialekto, firstnumber=last]
symbol Sequent : TYPE;
symbol ⊧ : List formula → List formula → Sequent;
notation ⊧ infix 50;
	\end{lstlisting}
	The \textit{proof steps} of Sequent Calculus are depicted in \autoref{fig:scsteps1}, \autoref{fig:scsteps2} and \autoref{fig:scsteps3}. There are other formalizations of Sequent Calculus, including some where $\Gamma$ and $\Delta$ are \textit{sets} rather than list,as justified by the \texttt{Contract} and \texttt{Swap} rules, but this formalism is best suited for encoding in Dedukti and is the one we assume in this paper.
	We call the rules in \autoref{fig:scsteps1} \textit{structural rules}. We call rules in \autoref{fig:scsteps2} introduction rules. Each of them correspond to the introduction of a logical symbol on the left or right hand side of the sequent.
	We call the rules in \autoref{fig:scsteps3} \textit{bonus rules}. These are not typically presented as part of sequent calculus. 
	The \texttt{Inst} rule for schematic symbols will naturally correspond to beta-reduction, as shown in \autoref{sect:encoding}.
	Since our language is first order logic \textit{with equlity}, the two \texttt{Equality} rules are necessary to encode the properties of equality. the two \texttt{IffSubst} rules describe the substitution of identical formulas for identical formulas. This is an admissible rule in first order logic without schematic symbols, as $\leftrightarrow$ is a congruence relation for logical operators. In presence of schematic connector symbols, this rule is sound but not admissible. We detail the question more in \autoref{sect:propext}, when we describe the axiom of propositional extensionality.
	
\begin{figure}
    \begin{center}
        \begin{tabular}{l l}
        	\AxiomC{$\Gamma, \phi, \psi, \Sigma \vdash \Delta$}
            \RightLabel{\text { LeftSwap} }
            \UnaryInfC{$\Gamma, \psi, \phi, \Sigma \vdash \Delta$}
            \DisplayProof &
            \AxiomC{$\Gamma \vdash \Delta, \phi, \psi, \Pi$}
            \RightLabel{\text { RightSwap} }
            \UnaryInfC{$\Gamma \vdash \Delta, \phi, \psi, \Pi$}
            \DisplayProof
            \\[5ex]
            
            \AxiomC{$\phi, \phi, \Gamma \vdash \Delta$}
            \RightLabel{\text { LeftContract} }
            \UnaryInfC{$\phi, \Gamma \vdash \Delta$}
            \DisplayProof &
            \AxiomC{$\Gamma \vdash \phi, \phi, \Delta$}
            \RightLabel{\text { RightContract} }
            \UnaryInfC{$\Gamma \vdash \phi, \Delta$}
            \DisplayProof
            \\[5ex]
            
            \AxiomC{}
            \RightLabel{\text { Hypothesis}}
            \UnaryInfC{$\Gamma, \phi \vdash \phi, \Delta$}
            \DisplayProof &
            \AxiomC{$\Gamma_1 \vdash \Delta_1$}
            \RightLabel{\text { Weakening} }
            \UnaryInfC{$\Gamma_2 \vdash \Delta_2$}
            \DisplayProof
            \\[5ex]
            
            \multicolumn{2}{c}{
                \AxiomC{$\Gamma \vdash \phi, \Delta$}
                \AxiomC{$\Sigma, \phi \vdash \Pi$}
                \RightLabel{\text{ Cut}}
                \BinaryInfC{$\Gamma, \Sigma \vdash \Delta, \Pi$}
                \DisplayProof
            }
        \end{tabular}
    \end{center}
\caption{Sructural rules of Sequent Calculus}
\label{fig:scsteps1}
\end{figure}


\begin{figure}
	
    \begin{center}
        \begin{tabular}{l l}
            \AxiomC{$\Gamma, \phi, \psi \vdash \Delta$}
            \RightLabel{\text { LeftAnd}}
            \UnaryInfC{$\Gamma, \phi \land \psi \vdash \Delta$}
            \DisplayProof &
            \AxiomC{$\Gamma \vdash \phi, \Delta$}
            \AxiomC{$\Sigma \vdash \psi, \Pi$}
            \RightLabel{\text{ RightAnd}}
            \BinaryInfC{$\Gamma, \Sigma \vdash \phi \land \psi,  \Delta, \Pi$}
            \DisplayProof
            \\[5ex]

            \AxiomC{$\Gamma, \phi \vdash \Delta$}
            \AxiomC{$\Sigma, \psi \vdash \Pi$}
            \RightLabel{\text{ LeftOr}}
            \BinaryInfC{$\Gamma, \Sigma, \phi\lor \psi \vdash \Delta, \Pi$}
            \DisplayProof &
            \AxiomC{$\Gamma \vdash \phi, \psi, \Delta$}
            \RightLabel{\text{ RightOr}}
            \UnaryInfC{$\Gamma \vdash \phi \lor \psi,  \Delta$}
            \DisplayProof
            \\[5ex]

            \AxiomC{$\Gamma \vdash \phi, \Delta$}
            \AxiomC{$\Sigma, \psi \vdash \Pi$}
            \RightLabel{\text{ LeftImplies}}
            \BinaryInfC{$\Gamma, \Sigma, \phi\rightarrow \psi \vdash \Delta, \Pi$}
            \DisplayProof &
            \AxiomC{$\Gamma, \phi \vdash \psi, \Delta$}
            \RightLabel{\text{ RightImplies}}
            \UnaryInfC{$\Gamma \vdash \phi \rightarrow \psi,  \Delta$}
            \DisplayProof
            \\[5ex]

            \AxiomC{$\Gamma, \phi \rightarrow \psi \vdash \Delta$}
            \RightLabel{\text { LeftIff}}
            \UnaryInfC{$\Gamma, \phi \leftrightarrow \psi \vdash \Delta$}
            \DisplayProof &
            \AxiomC{$\Gamma \vdash \phi \rightarrow \psi, \Delta$}
            \AxiomC{$\Sigma \vdash \psi \rightarrow \phi, \Pi$}
            \RightLabel{\text{ RightIff}}
            \BinaryInfC{$\Gamma, \Sigma \vdash \phi \leftrightarrow \psi,  \Delta, \Pi$}
            \DisplayProof
            \\[5ex]

            \AxiomC{$\Gamma \vdash \phi, \Delta$}
            \RightLabel{\text { LeftNot}}
            \UnaryInfC{$\Gamma, \neg \phi \vdash \Delta$}
            \DisplayProof &
            \AxiomC{$\Gamma, \phi \vdash \Delta$}
            \RightLabel{\text{ RightNot}}
            \UnaryInfC{$\Gamma \vdash \neg \phi ,  \Delta$}
            \DisplayProof
            \\[5ex]

            \AxiomC{$\Gamma, \phi[t := \schem{x}] \vdash \Delta$}
            \RightLabel{\text { LeftForall}}
            \UnaryInfC{$\Gamma, \forall \schem{x}. \phi  \vdash \Delta$}
            \DisplayProof &
            \AxiomC{$\Gamma \vdash \phi, \Delta$}
            \RightLabel{\text { RightForall}}
            \UnaryInfC{$\Gamma \vdash \forall \schem{x}. \phi,  \Delta$}
            \DisplayProof
            \\[5ex]

            \AxiomC{$\Gamma, \phi \vdash \Delta$}
            \RightLabel{\text { LeftExists}}
            \UnaryInfC{$\Gamma, \exists \schem{x}. \phi \vdash \Delta$}
            \DisplayProof &
            \AxiomC{$\Gamma \vdash \phi[t := \schem{x}], \Delta$}
            \RightLabel{\text { RightExists}}
            \UnaryInfC{$\Gamma \vdash \exists \schem{x}. \phi,  \Delta$}
            \DisplayProof
            \\[5ex]
		\end{tabular}
    \end{center}
\caption{Introduction rules of Sequent Calculus}
\label{fig:scsteps2}
\end{figure}

\begin{figure}

    \begin{center}
        \begin{tabular}{l l}
            \multicolumn{2}{c}{
                \AxiomC{$\Gamma \vdash \Delta$}
                \RightLabel{\text{ InstSchema}}
                \UnaryInfC{$\Gamma[\psi(\vec{v}) := {\schem{p}(\vec{v})}] \vdash \Delta[\psi(\vec{v}) := {\schem{p}(\vec{v})}]$}
                \DisplayProof 
            }\\[5ex]

            \AxiomC{$\Gamma, \phi[s := \schem{f}] \vdash \Delta$}
            \RightLabel{\text{ LeftSubstEq}}
            \UnaryInfC{$\Gamma, s=t, \phi[t := \schem{f}] \vdash \Delta$}
            \DisplayProof &
            \AxiomC{$\Gamma \vdash \phi[s := \schem{f}], \Delta$}
            \RightLabel{\text{ RightSubstEq}}
            \UnaryInfC{$\Gamma, s=t \vdash \phi[t := \schem{f}], \Delta$}
            \DisplayProof
            \\[5ex]

            \AxiomC{$\Gamma, \phi[a := {\schem{p}}] \vdash \Delta$}
            \RightLabel{\text{ LeftSubstIff}}
            \UnaryInfC{$\Gamma, a \leftrightarrow b, \phi[b := {\schem{p}}] \vdash \Delta$}
            \DisplayProof &
            \AxiomC{$\Gamma \vdash \phi[a := {\schem{p}}], \Delta$}
            \RightLabel{\text{ RightSubstIff}}
            \UnaryInfC{$\Gamma, a \leftrightarrow b \vdash \phi[b := {\schem{p}}], \Delta$}
            \DisplayProof
            \\[5ex]

            \AxiomC{$\Gamma, t = t \vdash \Delta$}
            \RightLabel{\text { LeftRefl}}
            \UnaryInfC{$\Gamma \vdash \Delta$}
            \DisplayProof &
            \AxiomC{}
            \RightLabel{\text{ RightRefl}}
            \UnaryInfC{$\vdash t=t$}
            \DisplayProof
            \\[5ex]

        \end{tabular}
    \end{center}
\caption{Bonus rules of Sequent Calculus}
\label{fig:scsteps3}
\end{figure}

	
\newpage

	\section{Encoding of Sequent calculus in Dedukti}
	\label{sect:encoding}
	We define the (dependent) type of the proofs of a particular sequent:
	\begin{lstlisting}[language=Dialekto, firstnumber=last]
symbol prf : Sequent → TYPE;
	\end{lstlisting}
	Each deduction rules of 

		
	We have already defined first-order formula.
	
	As we have done for natural numbers, we declare a type of formula at the level of Set in order to define a list of formulas
	
	\lstinputlisting[language=Dialekto, firstnumber=last, linerange={5-6}]{SimpleVersion/FOL.lp}
	
	
	
	\lstinputlisting[language=Dialekto, firstnumber=last, linerange={28-29}]{SimpleVersion/FOL.lp}
	
	\lstinputlisting[language=Dialekto, firstnumber=last, linerange={31-31}]{SimpleVersion/FOL.lp}
	
	
	
	\section{Link with other logics}
	
	\subsection{Minimalistic}
	
	\lstinputlisting[language=Dialekto, firstnumber=last, linerange={1-200}]{SimpleVersion/InterpretationMinimalistic.lp}
	
	
	\subsection{Intuitionistic}
	
	\lstinputlisting[language=Dialekto, firstnumber=last, linerange={1-200}]{SimpleVersion/InterpretationIntuitionistic.lp}
	
	\subsection{Classic}
	
	
	\section{Alternative}
	
	A sequent is a pair of finite lists which can be noted as follows: $H_1,...,H_m \vdash C_1,...,C_n$, where $H_i$ are hypotheses and $C_j$ are conclusions, $m \ge 0$ and $n \ge 0$.
	
	The usual interpretation of a sequent is
	$H_1 \land ... \land H_m \Rightarrow C_1 \lor ... \lor C_j$.
	
	As the logical connectives $\land$ and $\lor$ are commutative, it is also suitable to consider that a sequent is a pair of sets.
	
	However, as a set respects the properties of associative, commutative, unity and idempotence, it is less convenient to manage it with rewriting rules.
	To do that, we need to increase the expressivity of considered rewriting systems reasoning modulo ACUI.
	
	We implement 
	
	In practice, 
	
	AC ?
	
	\section{LISA}
	
	LISA is ...
	
	The proposed encoding can be seen as the first step to translate LISA into Dedukti as the encoded sequent calculus is similar to the one used for LISA.
	For now, LISA does not generate any kind of hints that are necessary to translate and recheck LISA proofs.
	
	The next step of this work is to instrument LISA in order to develop a translator from LISA to Dedukti.
	
	
	
	\section{Conclusion}
	
\end{document}