From 663bbfbee6e08e3fb9598e8305626f0d2a526f42 Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Fri, 24 Jun 2022 22:52:44 +0200
Subject: [PATCH] Clarifications, add motivation section

---
 spec/doc.tex | 53 ++++++++++++++++++++++++++++++++++------------------
 1 file changed, 35 insertions(+), 18 deletions(-)

diff --git a/spec/doc.tex b/spec/doc.tex
index 199ab17..691fb87 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -349,21 +349,32 @@ get in touch!
 
 \section{Introduction}
 
-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.
-The overall design follows a few core concepts, such as a natural-deduction
-style structure and rules generating and operating on ground first-order
-clauses.
+This document is a reference of the Alethe 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,
+such as interactive theorem provers or proof checkers.  The overall design
+follows a few core concepts, such as a natural-deduction style structure
+and rules generating and operating on ground first-order clauses.
 %
-There are two parts in this document: the proof language and a proof calculus.
-Section~\ref{sec:language} introduces the language.  First informally,
-then formally.
+The Alethe calculus consists of two parts: the proof language based on
+SMT-LIB and a collection of proof rules.
+Section~\ref{sec:language} introduces the language.  First as an abstract language,
+then as a concrete syntax.
 %
 Section~\ref{sec:rules-generic} discusses the core
-concepts behind the Alethe proof calculus.
+concepts behind the Alethe proof rules.
 %
-At the end of the document Section~\ref{sec:rules} presents a list of all proof
-rules used by SMT solvers supporting Alethe.
+At the end of the document Section~\ref{sec:rules} presents a list of
+all proof rules used by SMT solvers supporting Alethe.
+
+Alethe follows a few core design principles.  First, proofs should
+be easy to understand by humans to ensure working with Alethe proofs
+is effortless.  Second, the logic of the format should directly
+correspond to the logic used by the solver.  Since many solvers use the
+SMT-LIB logic, Alethe also uses this logic.  Third, the language should
+be uniform for all theories used by SMT solvers.  With the expectation
+of clauses for propositional reasoning, there is dedicated syntax for
+any logic
 
 The semantics (Section~\ref{sec:semantic}) and concrete syntax
 (Section~\ref{sec:syntax}) are based on the SMT-LIB~\cite{SMTLIB}
@@ -445,7 +456,8 @@ equality predicate.
 To simplify the
 notation we will omit the sort of terms when possible.
 
-\begin{example} The following example shows a simple Alethe proof.
+\begin{example} The following example shows a simple Alethe proof
+expressed in the abstract claculus used in this document.
 It uses quantifier instantiation and resolution to show a contradiction.
 The sections below step-by-step describe the concepts necessary to
 understand the proof intuitively.
@@ -500,11 +512,14 @@ the quantifier. Step 4 translates the disjunction into a clause.
 In the example above, the contexts are all empty.
 
 \paragraph{Assumptions.}
-The \proofRule{assume} command introduces a term as an assumption. The
-proof starts with a number of \proofRule{assume} commands. Each such command
+A \proofRule{assume} step introduces a term as an assumption. The
+proof starts with a number of \proofRule{assume} steps. Each such step
 corresponds to an input assertion. Additional assumptions can be introduced
 too. In this case each assumption must be discharged with an appropriate
-step. The rule \proofRule{subproof} can be used to do so.
+step. The rule \proofRule{subproof} can be used to do so.  In the concrete
+syntax \proofRule{assume} steps have a dedicated command $\grT{assume}$ to
+clearly distinguish them from normal steps that use the $\grT{step}$ command
+(see Section~\ref{sec:syntax}).
 
 The example above uses two assumptions which are introduced in the first
 two steps.
@@ -917,7 +932,9 @@ instantiation and resolution steps (line 10--15)}\label{fig:proof_ex}
 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.
+The format follows the SMT-LIB standard when possible.  Hence, beside
+the SMT-LIB logic and term language, it also uses commands to structure
+the proof.  An Alethe proof is a list of commands.
 
 Figure~\ref{fig:grammar} shows the grammar of the proof text. It
 is based on the SMT-LIB grammar, as defined in the SMT-LIB
@@ -1173,8 +1190,8 @@ resolution steps.
 To express quantifier instantiation, the rule \proofRule{forall\_inst}
 is used. It produces a formula of the form $(\neg \forall \bar
 x_n.\,\varphi)\lor \varphi[\bar t_n]$, where $\varphi$ is
-a term containing the free variables $\bar x_n$, and each $t_i$
-is a new ground term with the same sort as $x_i$ for each $i$.
+a term containing the free variables $\bar x_n$, and for each $i$ the
+ground term $t_i$ is a new term with the same sort as $x_i$.
 
 The arguments of a \proofRule{forall\_inst} step is the list \((x_1 , t_1),
 \dots, (x_n, t_n)\). While this information can be recovered from the term,
-- 
GitLab