From 08734cb44db6121121269683d0e90d34c69a066f Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Thu, 15 Jul 2021 14:33:26 +0200
Subject: [PATCH] Remove ugly \formatname macro, Alethe is now established
---
spec/doc.tex | 38 ++++++++++++++++++--------------------
1 file changed, 18 insertions(+), 20 deletions(-)
diff --git a/spec/doc.tex b/spec/doc.tex
index 541b134..c88deed 100644
--- a/spec/doc.tex
+++ b/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}
--
GitLab