Remove ugly \formatname macro, Alethe is now established

spec/doc.tex

@@ -59,8 +59,6 @@
 % ========================================
 % Commands
 % ========================================
- 
-\newcommand{\formatName}{Alethe}
 
 % Environment for discussion, conditional
 \ifdef{\nocomments}
@@ -271,7 +269,7 @@ break
 % Document
 % ========================================
 
-\title{The {\formatName} Proof Format}
+\title{The Alethe Proof Format}
 \subtitle{A Speculative Specification and Reference}
 \author{Haniel Barbosa\textsuperscript{1}
 \and Mathias Fleury\textsuperscript{2}
@@ -335,7 +333,7 @@ authors of those tools and we are committed to improve the tools, the
 format, and ultimately the specification together.
 This document is also an invitation to other researchers to join
 the efforts. To read the reference and provide feedback, or to even
-implement support for {\formatName} into their own tools. Please
+implement support for Alethe into their own tools. Please
 get in touch!
 
 \bigskip
@@ -344,7 +342,7 @@ get in touch!
 
 \section{Introduction}
 
-This document is a reference of the {\formatName} format.  The format
+This document is a reference of the Alethe format.  The format
 is designed to be a flexible format to represent unsatisfiability
 proofs generated by SMT solvers. It is designed around a few core
 concepts, such as a natural-deduction style structure and resolution.
@@ -358,16 +356,16 @@ format, which is widely used as input and output format of SMT
 solvers. Hence, the base logic is the many-sorted first-order logic of
 SMT-LIB. This document assumes the reader is familiar with the SMT-LIB
 standard.  As discussed in Section~\ref{sec:syntax} the concrete syntax
-of {\formatName} is based on the SMT-LIB syntax.
+of Alethe is based on the SMT-LIB syntax.
 
 The format is currently used by the CDCL($T$)-based SMT solver
 veriT~\cite{verit}. If requested by the user, veriT outputs a proof if it can
 deduce that the input problem is unsatisfiable. In proof production mode, veriT
 supports the theory of uninterpreted functions, the theory of linear integer and
-real arithmetic, and quantifiers.  The {\formatName} proofs can be reconstructed
+real arithmetic, and quantifiers.  The Alethe proofs can be reconstructed
 by the \texttt{smt} tactic of the proof assistant
 Isabelle/HOL~\cite{fleury-2019,schurr-2021}.  Furthermore, in the future the SMT
-solver cvc5 (the successor of CVC4~\cite{CVC4}) will support {\formatName} as
+solver cvc5 (the successor of CVC4~\cite{CVC4}) will support Alethe as
 one of multiple proof output formats.
 
 In addition to this reference, the proof format has been discussed in past
@@ -380,9 +378,9 @@ for processing, such as Skolemization, renaming of variables, and other
 manipulations of bound variables~\cite{barbosa-2019}.
 
 At the end of the document Section~\ref{sec:rules} contains a full list
-of all proof rules used by SMT solvers supporting {\formatName}.
+of all proof rules used by SMT solvers supporting Alethe.
 
-\section{Core Concepts of {\formatName}}
+\section{Core Concepts of Alethe}
 \label{sec:coreconcepts}
 
 This section provides an overview of the core concepts of the proof
@@ -394,13 +392,13 @@ practitioners.
 \paragraph{Multi-Sorted First-Order Logic.}
 
 Many SMT solvers use the SMT-LIB language~\cite{SMTLIB} as both its
-input and output language and {\formatName} builds on this language.
+input and output language and Alethe builds on this language.
 This includes its multi-sorted first-order logic.  The available sorts
 depend on the selected SMT-LIB theory/logic and they can also be extended by the
 user, but a distinguished $\mathbf{Bool}$ sort is always available.
 
 In addition to the multi-sorted first-order logic used by SMT-LIB,
-{\formatName} also uses Hilbert's choice operator $\varepsilon$. Choice acts
+Alethe also uses Hilbert's choice operator $\varepsilon$. Choice acts
 like a binder. The term $\varepsilon x. \varphi$ stands for a value $v$,
 such that $\varphi[v/x]$ is true if such a value exists. Any value is
 possible otherwise.
@@ -422,7 +420,7 @@ for $\varphi$ and odd for $\psi$, or vice versa.  To simplify the
 notation we will omit the sort of terms when possible.
 
 \paragraph{Steps.}
-A proof in the {\formatName} format is an indexed list of steps.
+A proof in the Alethe format is an indexed list of steps.
 To mimic the concrete syntax we will write a step
 \begin{plListEq}
 	c_1,\,\dots,\, c_k &\proofsep i. & \varphi_1,\dots ,\varphi_l &
@@ -463,7 +461,7 @@ too. In this case each assumption must be discharged with an appropriate
 step. The only rule to do so is the \proofRule{subproof} rule.
  
 \paragraph{Subproofs and Lemmas.}
-{\formatName} uses subproof to prove lemmas and to manipulate the context.
+Alethe uses subproof to prove lemmas and to manipulate the context.
 To prove lemmas, a subproof can
 introduce local assumptions. The subproof \emph{rule} discharges the
 local assumptions.
@@ -542,7 +540,7 @@ it deduces $\neg \varphi_1 \lor \varphi_2$.
 
 \paragraph{Resolution.}
 CDCL($T$)-based SMT solvers, and especially their SAT solvers,
-are fundamentally based on clauses. Hence, {\formatName} also uses
+are fundamentally based on clauses. Hence, Alethe also uses
 clauses.  Nevertheless, since SMT solvers do not enforce a strict
 clausal normal-form, ordinary disjunction is also used.
 Keeping clauses and disjunctions distinct, simplifies rule checking.
@@ -555,7 +553,7 @@ use the standard SMT-LIB \smtinline{or} operator. The \proofRule{or}
 
 % PF TODO: I would fix that just now, using an attribute to distinguish, and a
 % unique rule
-The {\formatName} proofs use a generalized propositional
+The Alethe proofs use a generalized propositional
 resolution rule with the rule name \proofRule{resolution} or
 \proofRule{th\_resolution}. Both names denote the same rule. The
 difference only serves to distinguish if the rule was introduced by
@@ -695,7 +693,7 @@ when the term below the equality changes during proof search. One such
 case is the instantiation of universally quantified variables. If an
 instantiated variable appears below an equality, then the equality might
 have an arbitrary order after instantiation.
-Nevertheless, consumers of {\formatName} must consider the possible
+Nevertheless, consumers of Alethe must consider the possible
 implicit reordering of equalities.
 
 % PF TODO why concrete?  Why not simply call it Semantics?
@@ -985,7 +983,7 @@ instantiation and resolution steps (line 10--15)}\label{fig:proof_ex}
 \section{The Concrete Syntax}
 \label{sec:syntax}
 
-The concrete text representation of the {\formatName}  proofs
+The concrete text representation of the Alethe proofs
 is based on the SMT-LIB standard. Figure~\ref{fig:proof_ex} shows an
 exemplary proof as printed by veriT with light edits for readability.
 The format follows the SMT-LIB standard when possible.
@@ -1186,7 +1184,7 @@ no $\grT{define-fun}$ commands are issued and the constants are expanded.
 \label{sec:rules-overview}
 
 Section~\ref{sec:rules} provides a list of all proof rules supported by
-{\formatName}.  To make this long list more accessible, this section
+Alethe.  To make this long list more accessible, this section
 first lists multiple classes of proof rules.  The classes are not
 mutually exclusive: for example, the \proofRule{la\_generic} rule is
 both a linear arithmetic rule and introduces a tautology.
@@ -1433,7 +1431,7 @@ Rule & Description \\
 \section{List of Proof Rules}
 \label{sec:rules}
 
-The following lists all rules of {\formatName}.
+The following lists all rules of Alethe.
 
 \input{rule_list}