From 2a770483dcf2806bf7a74780faf243ba4cf57ee6 Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Thu, 23 May 2024 18:23:32 -0500
Subject: [PATCH] Add condensed syntax for numbers and explain
---
spec/doc.tex | 46 +++++++++++++++++++++++++++++++++++++++++-----
1 file changed, 41 insertions(+), 5 deletions(-)
diff --git a/spec/doc.tex b/spec/doc.tex
index b826c03..e230fa7 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -647,7 +647,7 @@ The concrete text representation of the Alethe proofs
is based on the {\smtlib} standard. Figure~\ref{fig:proof_ex} shows an
example proof as printed by {\verit} with light edits for readability.
%
-The format follows the {\smtlib} standard when possible.
+The format broadly follows the {\smtlib} standard.
%
Input problems in the {\smtlib} format are scripts. An {\smtlib} script
is a list of commands that manipulate the SMT solver. For example,
@@ -704,6 +704,7 @@ An Alethe proof is a list of commands.
\grNT{clause} &\grRule & \textAlethe{(cl}\; \grNT{proof\_term}^{*}\,\textAlethe{)} \\
\grNT{proof\_term} &\grRule & \grNT{term}\text{ extended with } \\
& & \textAlethe{(choice (}\, \grNT{sorted\_var}\,\textAlethe{)}\; \grNT{proof\_term}\,\textAlethe{)} \\
+ & \grOr & \grNT{rational}\;\grOr\;\grNT{neg\_numeral}\;\grOr\;\grNT{neg\_decimal} \\
\grNT{premises\_annotation} &\grRule & \textAlethe{:premises (}\; \grNT{symbol}^{+}\textAlethe{)} \\
\grNT{args\_annotation} &\grRule & \textAlethe{:args}\,\textAlethe{(}\,\grNT{step\_arg}^{+}\,\textAlethe{)} \\
\grNT{step\_arg} &\grRule & \grNT{symbol}\;\grOr\;
@@ -711,13 +712,16 @@ An Alethe proof is a list of commands.
\grNT{context\_annotation} &\grRule & \textAlethe{:args}\,\textAlethe{(}\,\grNT{context\_assignment}^{+}\,\textAlethe{)} \\
\grNT{context\_assignment} &\grRule & \grNT{sorted\_var} \\
& \grOr & \textAlethe{(:=}\, \grNT{sorted\_var}\;\grNT{proof\_term}\,\textAlethe{)} \\
+ \grNT{rational} &\grRule & -^{?}\grNT{numeral}/\grNT{numeral} \\
+ \grNT{neg\_numeral} &\grRule & -\grNT{numeral} \\
+ \grNT{neg\_decimal} &\grRule & -\grNT{decimal} \\
\end{array}
\]
\caption{The proof grammar.}
\label{fig:grammar}
\end{figure}
-Every Alethe proof is associated with an {\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
@@ -743,9 +747,7 @@ $\grNT{function\_def}$,
$\grNT{sorted\_var}$,
$\grNT{symbol}$, and
$\grNT{term}$
-are as defined in the standard. The non-terminal $\grNT{proof\_term}$
-corresponds to the $\grNT{term}$ non-terminal of {\smtlib}, but is
-extended with the additional production for the \inlineAlethe{choice}\index{choice} binder.
+are as defined in the standard.
Alethe proofs are a list of commands.
The \inlineAlethe{assume} command introduces a new assumption. While this
@@ -800,6 +802,36 @@ annotations. This can be used for debugging, or other purposes.
A consumer of Alethe proofs {\em must} be able to parse proofs
that contain such annotations.
+\paragraph{Terms}
+The non-terminal $\grNT{proof\_term}$ is an extended version of the {\smtlib}
+non-terminal $\grNT{term}$.
+First, it has an additional production for the
+\inlineAlethe{choice}\index{choice} binder.
+%
+Second, it has productions to express rationals and negative integers
+concisely.
+%
+A difficulty when parsing {\smtlib} terms is that numerical constants
+are not easy to distinguish from general terms.
+For example, $-\frac{1}{2}$ is written as
+\inlineAlethe{(/ (- 1) 2)}.
+The $\grNT{rational}$ non-terminal makes it possible to write this constant
+as a single literal: \inlineAlethe{-1/2}.
+Furthermore, the non-terminals $\grNT{neg\_numeral}$ and $\grNT{neg\_decimal}$
+achieve the same for unary negation.
+
+The sorting rules for $\grNT{proof\_term}$ are as for {\smtlib} terms with
+one key difference.
+The sort of terms produced by $\grNT{rational}$, $\grNT{decimal}$, and
+$\grNT{neg\_decimal}$ is always \inlineAlethe{Real}.
+The sort of terms produced by $\grNT{integer}$ and $\grNT{neg\_integer}$
+is always \inlineAlethe{Int}.
+For example, in standard {\smtlib}, the term \inlineAlethe{(+ 5 3)}
+has the sort \inlineAlethe{Int} in the logic \texttt{QF\_LIA}, but
+has the sort \inlineAlethe{Real} in \texttt{QF\_LRA}.
+In Alethe, this term always has the sort \inlineAlethe{Int},
+and would not be well sorted in the logic \texttt{QF\_LRA}.
+
\paragraph{Subproofs}
The abstract notation denotes subproofs by marking them with a vertical
line. To map this notation to a list of commands, Alethe \index{anchor}uses the
@@ -983,8 +1015,12 @@ Overall, the following aspects are treated implicitly by Alethe.
introduces {\verit} to print Skolem terms as defined functions. User defined
functions in the input problem are not supported by {\verit} in proof production
mode.}
+ \item If the input problem is in a logic without integers, then constants from
+ $\grNT{numeral}$ in the input problem will be printed using
+ $\grNT{decimal}$ or $\grNT{rational}$ in the proof.
\end{itemize}
+\noindent
Alethe proofs contain steps for other aspects that are commonly left implicit, such
as renaming of bound variables, and the application of substitutions.
--
GitLab