From de29f8f1a9760fe3fe02b16aa0c55cec81ee1afa Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Tue, 6 Aug 2024 18:38:39 -0500
Subject: [PATCH] Clarify that symbols that overlap with numbers are not
allowed
---
spec/changelog.tex | 12 +++++-------
spec/doc.tex | 23 ++++++++++++++++++-----
2 files changed, 23 insertions(+), 12 deletions(-)
diff --git a/spec/changelog.tex b/spec/changelog.tex
index c0d9349..807045a 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -22,7 +22,7 @@ Breaking changes:
be \texttt{(x S) (:= (y S) x)}.
\item The arguments for \proofRule{forall_inst} have been changed to
no longer take the shape of bindings using \texttt{(:= x c)}.
- Instead, the list of instatiation terms must follow the variable
+ Instead, the list of instantiation terms must follow the variable
order and cover all the respective bound variables.
\item The rules \proofRule{and_pos}, \proofRule{or_neg}, \proofRule{and},
\proofRule{not_or} now have one argument that indicates which subterm
@@ -31,12 +31,10 @@ Breaking changes:
for \proofRule{la_generic}.
\item Restrict sorting of numbers such that the sort of a constant is
only determined by its syntactic category.
- \item The arguments for \proofRule{forall_inst} have been changed to
- no longer take the shape of bindings using \texttt{(:= x c)}.
- Instead, the list of instatiation terms must follow the variable
- order and cover all the respective bound variables.
- \item Add new syntax for decimal and negative numbers and use it
- for \proofRule{la_generic}.
+ \item Add new syntax for decimal and negative numbers and clarify that
+ the set of allowed symbols is restricted to not conflict with this
+ new syntax.
+ \item Always use decimals for the constants in \proofRule{la_generic}.
\item Restrict sorting of numbers such that the sort of a constant is
only determined by its syntactic category.
\end{itemize}
diff --git a/spec/doc.tex b/spec/doc.tex
index be140d5..9f59ddc 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -691,6 +691,12 @@ An Alethe proof is a list of commands.
\begin{figure}[t]
\[
\begin{array}{r c l}
+
+\multicolumn{3}{c}{
+ \text{A }\grNT{symbol}\text{ is an SMT-LIB }\grNT{symbol}\text{ that is not a}}\\
+& & -\grNT{numeral}/\grNT{positive\_numeral},\\
+& & -\grNT{numeral},\text{ or} -\grNT{decimal}.\\
+
\grNT{proof} &\grRule & \grNT{proof\_command}^{*} \\
\grNT{proof\_command} &\grRule & \textAlethe{(assume}\; \grNT{symbol}\; \grNT{proof\_term}\;\grNT{attribute}^{*}\,\textAlethe{)} \\
&\grOr & \textAlethe{(step}\; \grNT{symbol}\; \grNT{clause}
@@ -715,9 +721,9 @@ An Alethe proof is a list of commands.
\grNT{context\_assignment} &\grRule & \grNT{sorted\_var} \\
& \grOr & \textAlethe{(:=}\, \grNT{sorted\_var}\;\grNT{proof\_term}\,\textAlethe{)} \\
\grNT{positive\_numeral} &\grRule & \text{any }\grNT{numeral}\text{ except } 0\\
- \grNT{rational} &\grRule & -^{?}\grNT{numeral}/\grNT{positive\_numeral} \\
- \grNT{nonpositive\_numeral} &\grRule & -\grNT{numeral} \\
- \grNT{nonpositive\_decimal} &\grRule & -\grNT{decimal} \\
+ \grNT{rational} &\grRule & -^{?}\grNT{numeral}/\grNT{positive\_numeral} \\
+ \grNT{nonpositive\_numeral} &\grRule & -\grNT{numeral} \\
+ \grNT{nonpositive\_decimal} &\grRule & -\grNT{decimal} \\
\end{array}
\]
\caption{The proof grammar.}
@@ -747,10 +753,17 @@ is based on the {\smtlib} grammar, as defined in the {\smtlib}
standard~\cite[Appendix~B]{SMTLIB}. The non-terminals
$\grNT{attribute}$,
$\grNT{function\_def}$,
-$\grNT{sorted\_var}$,
-$\grNT{symbol}$, and
+$\grNT{sorted\_var}$, and
$\grNT{term}$
are as defined in the standard.
+A special restriction applies to the $\grNT{symbol}$ non-terminal.
+Alethe has an extended set of number literals. Since these can start
+with a negation sign, they overlap SMT-LIB's $\grNT{symbol}$ non-terminal.
+For example, \inlineAlethe{-1} is a valid $\grNT{symbol}$ in SMT-LIB.
+These sequences cannot be used as symbols when using Alethe.
+Note that symbols are also used to name user defined constants and functions
+in the input problem. Hence, Alethe cannot express proofs about problems
+that use such symbols.
Alethe proofs are a list of commands.
The \inlineAlethe{assume} command introduces a new assumption. While this
--
GitLab