Backport specification from my PhD thesis

This replaces the text of the specification and the rule list with the text in my PhD thesis.

Most importantly this adds an abstract proof checking procedure that specifies the semantic of an Altehe proof (modulo the proof rules).

Furthermore, it adapts the notation more to SMT-LIB: everything is in λ-application style ((f x) instead of f(x)) and we no longer have a distinct connective. Instead we use the equality predicate everywhere.

On the technical side this now requires lualatex for Unicode math.

spec/doc.tex

@@ -340,7 +340,7 @@ bound variables~\cite{barbosa-2019}.
 \subsection{Notations}
 
 The notation used in this document is similar to the notation
-used by the SMT-LIB standard.  The Alethe proof format uses precisely
+used by the SMT-LIB standard.  The Alethe proof format uses
 the SMT-LIB logic.  Since the SMT-LIB language is based on
 S-expressions\index{S-expression}, SMT-LIB formulas are written using
 a λ-calculus style.  That is, instead of $f(1,2)$, we write $(f\,1\,2)$.
@@ -353,30 +353,37 @@ $f, g$ for functions, and $P, Q$ for predicates (functions with co-domain
 sort $\lsymb{Bool}$.  To indicate terms we use $t, u$ and to indicate
 formulas (terms of sort $\lsymb{Bool}$) we use $\varphi, \psi$.
 To distinguish syntactic equality and the SMT-LIB equality predicate,
-we write $=$ for the former, and $≈$ for the later.
+we write $=$ for the former, and $≈$ for the latter.
 We will write pre-defined SMT-LIB symbols, such as sorts and functions,
 in bold (e.g., $\lsymb{Bool}$, $\lsymb{ite}$).
 
-We will use $θ$ to denote a
-substitution\index{substitution}.
+We will use $θ$ to denote a substitution\index{substitution}.
 The notation $[x₁ ↦ t₁, …, x_n ↦ t_n]$ denotes the substitution
 that maps $x_i$ to $t_i$ for $1 ≤ i ≤ n$ and corresponds to the
-identity function for all other variables.  If $θ$ and $η$ are two
+identity function for all other variables.
+%
+If $θ$ and $η$ are two
 substitutions, then $θη$ denotes the result of first applying $θ$
 and then $η$ (i.e., $η(θ(.))$).  A substitution can naturally be extended
 to a function that maps terms to terms by replacing the occurrences of
 free variables.
 %
-We write $t[\,]$ for a term with a hole\index{hole} and $t[u]$ for the term where
-the hole has been replaced by $u$. Any term has at most one hole.
+The application of a substitution $θ$ to a term $t$ (i.e., $θ(t)$)
+is capture-avoiding; bound variables in $t$ are renamed as necessary.
+
+We write $t[u]$ for a term that contains the term $u$ as a subterm.  If $u$
+is subsequently replaced by a term $v$, we write $t[v]$ for the
+new term.
 %
-We also use holes with multiple variables.
+We also use this notation with multiple terms.
 %
-The notation $t[x_1, \dots, x_n]$ stands for a term that may depend on distinct
-variables $x_1, \dots, x_n$.
+The notation $t[u_1, \dots, u_n]$ stands for a term may contain the
+pairwise distinct terms $u_1, \dots, u_n$.
 %
-$t[s_1,\dots, s_n]$ is the respective term where the variables $x_1,\dots, x_n$ are
-simultaneously substituted by $s_1,\dots, s_n$.
+Then, $t[s_1,\dots, s_n]$ is the respective term where the
+variables $u_1,\dots, u_n$ are
+simultaneously replaced by $s_1,\dots, s_n$.  Usually, $u_1, \dots, u_n$ will
+be variables.
 
 Note that we will introduce the Alethe specific notation to write proof steps
 in the following sections.
@@ -541,8 +548,7 @@ variable.  The second case is a mapping.
 Throughout this chapter, $\Gamma$ denotes
 an arbitrary context.
 
-% TODO: define \subst and related
-Every context $\Gamma$ induces a substitution
+Every context $\Gamma$ induces a capture-avoiding substitution
 $\subst(\Gamma)$. If $\Gamma$ is the empty list,
 $\subst(\Gamma)$ is the empty substitution, i.e, the
 identity function.
@@ -554,14 +560,13 @@ substitution for $x_n$:
 \]
 
 When $\Gamma$ ends in a mapping, the substitution is extended
-with this mapping:
+with this mapping\label{page:ctxdef}:
 \[
 \subst([c_1,\dots, c_{n-1}, x_n\mapsto t_n]) =
         \subst([c_1,\dots, c_{n-1}])\circ \{x_n\mapsto t_n\}.
 \]
 
-
-\label{ex:alethe:substctx}The following example illustrates this idea:
+\label{ex:alethe:substctx}The following example illustrates this idea.
 \begin{align*}
     \subst([x\mapsto 7, x \mapsto g(x)]) &= \{x\mapsto g(7)\} \\
     \subst([x\mapsto 7, x, x \mapsto g(x)]) &= \{x\mapsto g(x)\} \\
@@ -577,10 +582,15 @@ where the term $t$\, is the original term, and $u$ is the term after
 preprocessing.  Tautologies with contexts correspond to judgments
 $\vDash_T \subst(\Gamma)(t) ≈ u$.
 
+Since the substitution induced by a context is capture-avoiding,
+applying it might rename bound variables to avoid binding variables
+in substituent terms.
+This is an implicit term transformation without a proof.  Therefore,
+the Alethe rules are designed to avoid such contexts.
+
 Formally, the context can be translated to \index{abstraction!lambda}λ-abstractions and
 applications.  This is discussed in Section~\ref{sec:alethe:semantics}.
 
-
 \begin{example}\label{ex:ti:ctx-abstract}
 This example shows a proof that uses a subproof with a context to rename a bound
 variable.
@@ -697,8 +707,7 @@ An Alethe proof is a list of commands.
   \label{fig:grammar}
 \end{figure}
 
-
-Usually, an Alethe proof is associated with a concrete {\smtlib} problem
+Every Alethe proof is associated with an  {\smtlib} problem
 that is proved by the Alethe proof.  This can either be a concrete
 problem file or, if the incremental solving commands of {\smtlib}
 are used, the implicit problem constructed at the invocation of a
@@ -756,6 +765,8 @@ represent unary or empty clauses. To circumvent this, we introduce a new
 function
 extended to one argument, where it is equal to the identity, and zero
 arguments, where it is equal to \inlineAlethe{false}.
+Every step must use the \inlineAlethe{cl} operator, even if its conclusion
+is a unit clause.
 The \inlineAlethe{anchor} and \inlineAlethe{define-fun} commands are used for
 subproofs and sharing, respectively. The \inlineAlethe{define-fun} command
 corresponds exactly to the \inlineAlethe{define-fun} command of the
@@ -788,8 +799,6 @@ a \index{rule!concluding}{\em concluding rule}
 After the \inlineAlethe{anchor} command, the proof uses \inlineAlethe{assume} commands to list
 the assumptions of the subproof.  Subsequently, the subproof is a list of
 \inlineAlethe{step} commands that can use prior steps in the subproofs as premises.
-% the assumptions of any parent subproof
-% as premises.
 
 In the abstract notation, every step is associated with a context.  The
 concrete syntax uses anchors to optimize this.
@@ -803,12 +812,18 @@ corresponding \inlineAlethe{step} commands pop from the context.
 To indicate these changes to the context, every anchor is associated with a list
 of fixed variables and mappings.
 This list can be empty.
-
-The \inlineAlethe{:step} annotation of the anchor command is used to indicate the \inlineAlethe{step}
-command that will end the subproof.  The clause of this \inlineAlethe{step}
-command is the conclusion of the subproof.   While it is possible to infer the
+Note that, when an \inlineAlethe{anchor} command extends a context $\Gamma$ with
+some mappings $x_1 \mapsto t_1, \dots,  x_n \mapsto t_n$,
+then the terms $t_i$ are normalized by applying
+the substitution $\subst(\Gamma)$ to $t_i$.  This is because the definition
+on page~\pageref{page:ctxdef} extends the context by composing the substitutions.
+
+The \inlineAlethe{:step} annotation of the anchor command is used to indicate
+the \inlineAlethe{step} command that will end the subproof.  The clause of
+this \inlineAlethe{step} command is the conclusion of the subproof.
+While it is possible to infer the
 step that concludes a subproof from the structure of the proof, the explicit
-annotation simplifies reconstruction and makes the proof easier to read.
+annotation simplifies proof checking and makes the proof easier to read.
 If the subproof uses a
 context, the \inlineAlethe{:args} annotation of the \inlineAlethe{anchor} command
 indicates the arguments added to the context for this subproof.  The
@@ -1014,8 +1029,7 @@ It is easy to calculate the context of the first-innermost subproof.
 \begin{definition}[Calculated Context]
   Let $[C_{\mathit{start}}, \dots, C_{\mathit{end}}]$ be
   the first-innermost subproof of $P$.
-  For $\mathit{start} \leq i < \mathit{end}$, let
-  $A_1, \dots, A_m$ be the anchors among $C_1, \dots, C_{i-1}$.
+  Let $A_1, \dots, A_m$ be the anchors among $C_1, \dots, C_{\mathit{start}-1}$.
 
   The \index{context!calculated}calculated context of $C_i$ is the context
   \[
@@ -1317,7 +1331,7 @@ proofs.
 Here, $\vDash$ represents
 semantic consequence in the many-sorted first order logic of {\smtlib}
 with the theories of uninterpreted functions and linear arithmetic extended
-to clauses.
+with the choice operator and  clauses.
 
 To show the soundness of a valid Alethe proof $P = [C_1, \dots, C_n]$,
 we can use the same approach as for the definition of validity: consider
@@ -1550,11 +1564,11 @@ syntax for clauses uses the \inlineAlethe{cl} operator, while disjunctions
 use the standard {\smtlib} \inlineAlethe{or} operator. The \proofRule{or}
 \emph{rule} is responsible for converting disjunctions into clauses.
 
+The Alethe proofs use a generalized propositional resolution
+rule with the 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
 the SAT solver or by a theory solver. The resolution step is purely
-resolution rule with the 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
-The Alethe proofs use a generalized propositional
 propositional; there is no notion of a unifier.  The resolution
 rules also implicitly simplifies repeated negations at the head
 of literals.
@@ -1564,13 +1578,12 @@ is a clause that has been derived from the premises by some binary
 resolution steps.
 
 \paragraph{Quantifier Instantiation}
-\label{reference=rule:forall_inst}
 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 for each $i$ the
 ground term $t_i$ is a new term with the same sort as $x_i$.\footnote{
-  For historical reasons, \proofRule{forall} has a unit clause with a disjunction
+  For historical reasons, \proofRule{forall_inst} has a unit clause with a disjunction
   as its conclusion and not the clause $(\neg \forall \bar x_n.\,\varphi), \varphi[\bar t_n]$.
 }