Révision 254 CSL17/tech-report/intro.tex
| intro.tex (revision 254) | ||
|---|---|---|
| 55 | 55 |
%Then we describe an encoding of sequences which will be instrumental in the proof of our result. |
| 56 | 56 |
We present our arithmetic theories $\arith^i$ in Sect.~\ref{sect:arithmetic} and give our soundness result, that the provably total functions of $\arith^i$ are in $\fph_i$, in Sect.~\ref{sect:soundness}. Finally, we sketch the completeness result, that all $\fph_i$ functions have a representation provably total in $\arith^i$, in Sect.~\ref{sect:completeness}, and present conclusions in Sect.~\ref{sect:conclusion}.
|
| 57 | 57 |
|
| 58 |
We are able to include only brief accounts of our technical results in this paper due to space constraints, in particular for our soundness and completeness results, Thms.~\ref{sect:soundness} and \ref{thm:completeness} respectively.
|
|
| 59 |
More detailed proofs can be found in the technical report \cite{BaiDas17:fph-techreport}.
|
|
| 58 |
% We are able to include only brief accounts of our technical results in this paper due to space constraints, in particular for our soundness and completeness results, Thms.~\ref{sect:soundness} and \ref{thm:completeness} respectively.
|
|
| 59 |
% More detailed proofs can be found in the technical report \cite{BaiDas17:fph-techreport}.
|
|
| 60 | 60 |
|
| 61 | 61 |
|
| 62 | 62 |
% \patrick{
|
Formats disponibles : Unified diff