Remove introduction paragraph

This served as the introduction to the entire chapter in the
thesis.

spec/spec.tex

@@ -92,86 +92,10 @@ get in touch!
 \hspace*{\fill}The authors.
 \end{abstract}
 
-\end{document}
-If an {\smt} solver determines that an input problem is satisfiable,
-it might provide a model to the user.
-%
-If it determines that the problem is unsatisfiable, it might provide a
-proof that exhibits the unsatisfiability of the problem.
-%
-When an {\smt} solver is used by {\sledgehammer} or by the \tactic{smt} tactic,
-we are in the second scenario.
-%
-Both tools {\em negate} the current proof obligation, add the selected
-background lemmas, and encode the result as an {\smtlib} problem.
-%
-Hence, the {\smt} solver is successful if it can show the validity of
-the proof obligation and selected lemmas by showing the unsatisfiability
-of the generated problem.
-%
-While {\sledgehammer} is content with an unsatisfiability core during
-the filtering phase, the \tactic{smt} tactic needs a proof that
-it can reconstruct within the trusted kernel of {\isabelle}.
-
-This chapter discusses a proof format for {\smt} solvers and its
-reconstruction by the \tactic{smt} tactic.  The format is called
-\quotation{Alethe} and it builds upon earlier formats used by
-the solver {\verit}.
-%
-Proof production from {\verit} goes back ten years~\cite[besson-2011].
-%
-Since then, it was refined and
-extended.  Most notably, the proof format
-was extended with a notion of context to express reasoning with
-\index{binder}binders~\cite[barbosa-2019].
-
-
-The work on implementing the proof reconstruction for the \tactic{smt}
-tactic exposed shortcoming with the proofs generated by {\verit}. 
-First, there was no complete documentation and specification
-of the proof rules available.
-\in{Section}[sec:alethe] fills this gap -- it is a full documentation
-of the Alethe proof format.
-\in{Section}[sec:alethe] also
-clarifies the connection between abstract proofs and the
-concrete proofs produced by {\verit}.
-Second, some proof rules were hard to reconstruct and there were gaps in the proofs.
-In \in{Section}[sec:reconstruction] we discuss improvements to the format that solve
-these issues.
-We also used this effort to overhaul the concrete syntax of Alethe proofs.
-They now use a {\smtlib}-based syntax that uses a flat list of commands
-instead of a nested structure.
-
-Overall,
-\in{Section}[sec:reconstruction] discusses the reconstruction of
-Alethe proofs implemented by the \tactic{smt} tactic of {\isabelle}.
-%
-This section also discusses the aforementioned improvements to {\verit}'s proofs.
-%
-The empirical
-evaluation shows that the addition of {\verit} support to \tactic{smt} 
-reduces the number of preplay failures of the {\sledgehammer} pipeline.
 
-Overall, the implementation of the proof reconstruction was successful,
-because we also improved the proof format.
-%
-Accordingly, \in{Section}[sec:proof-re:future] we discuss both
-opportunities to improve the reconstruction and the Alethe
-proof format.
-
-
-% ================== Start cutoff
-
-\startsection[reference=sec:alethe,title=The Alethe Proof Format]
-\chapterannot{This section is based on an informally published reference
-of the Alethe proof format.
-It was originally written by me for the work in
-\in{Section}[sec:reconstruction].  Later\\ Haniel Barbosa,\\ Mathias Fleury, \\
-Pascal Fontaine contributed.
-}
-
-This section is a reference of the
-Alethe\footnote{Alethe is a genus of small birds that occur in West Africa~\cite[wp:alethe].   The name was chosen, because it
+This document is a reference of the
+Alethe\footnote{Alethe is a genus of small birds that occur in West Africa~\cite[wp:alethe].
+The name was chosen, because it
 resembles the Greek word αλήθεια (alítheia) -- truth.} proof format.  Alethe is
 designed to be a flexible format to represent unsatisfiability proofs
 generated by {\smt} solvers.  Alethe proofs can be consumed by other systems,
@@ -220,7 +144,7 @@ output formats.
 %
 Furthermore, there is an experimental
 high-performance proof checker written in Rust.\footnote{Available at
-\href{https://github.com/ufmg-smite/alethe-proof-checker}.}
+\url{https://github.com/ufmg-smite/alethe-proof-checker}.}
 
 In addition to this reference, the proof format has been discussed in past
 publications, which provide valuable background information.  The core of
@@ -232,6 +156,9 @@ More recently, the format has gained support for reasoning typically used for
 processing, such as skolemization, substitutions, and other manipulations of
 bound variables~\cite[barbosa-2019].
 
+\end{document}
+% ================== Start cutoff
+
 \subsection[sec:alethe:language]{The Alethe Language}
 
 This section provides an overview of the core concepts of the