diff --git a/spec/changelog.tex b/spec/changelog.tex
index 39049184b4a1a6239b7eefff773a6331ce1b3312..807045a2654d1f662ade02ad9f5a1b7defca0dc1 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -22,11 +22,21 @@ 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
they use.
+ \item Add new syntax for decimal and negative numbers and use it
+ for \proofRule{la_generic}.
+ \item Restrict sorting of numbers such that the sort of a constant is
+ only determined by its syntactic category.
+ \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}
\noindent
diff --git a/spec/doc.tex b/spec/doc.tex
index b826c03ec0e80ed1d4d61f8b2758b0e92ae234e3..9f59ddca81746c821c60341202e6ca2437e4317b 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -214,7 +214,7 @@ break
\textsuperscript{1} Universidade Federal de Minas Gerais, Brazil\\
\textsuperscript{2} Albert-Ludwig-Universität Freiburg, Germany\\
\textsuperscript{3} Université de Liège, Belgium\\
- \textsuperscript{4} University of Iowa, Iowa City, USA\\
+ \textsuperscript{4} The University of Iowa, Iowa City, USA\\
}
@@ -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,
@@ -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}
@@ -704,6 +710,9 @@ 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{nonpositive\_numeral} \\
+ & \grOr & \grNT{nonpositive\_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 +720,17 @@ 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{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} \\
\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
@@ -740,12 +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. 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.
+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
@@ -800,6 +818,35 @@ 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{nonpositive\_numeral}$ and $\grNT{nonpositive\_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{nonpositive\_decimal}$ is always \inlineAlethe{Real}.
+The sort of terms produced by $\grNT{integer}$ and $\grNT{nonpositive\_numeral}$
+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}.
+
\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 +1030,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.
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 44c309949e9638b1f5b7abae28816b04f69cf486..c226703eb54b2cc2a969770ef5910cc7ccfc8d56 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -427,9 +427,9 @@ $i$. & \ctxsep & $\varphi_1$, \dots , $\varphi_o$ & \currule\, [$a_1$, \dots, $
where $\varphi_i$ is either $\neg l_i$ or $l_i$, but never $s_1
≈ s_2$.
-If the current theory does not have rational numbers, then the $a_i$ are
-printed using integer division. They should, nevertheless, be interpreted
-as rational numbers. If $d_1$ or $d_2$ are $0$, they might not be printed.
+The constants $a_i$ are of sort \inlineAlethe{Real} and must be printed
+using one of the productions $\grNT{rational}$
+$\grNT{decimal}$, $\grNT{nonpositive\_decimal}$.
To check the unsatisfiability of the negation of $\varphi_1\lor \dots
\lor \varphi_o$ one performs the following steps for each literal. For
@@ -481,7 +481,7 @@ A simple \proofRule{la_generic} step in the logic \textsf{LRA} might look like t
\begin{AletheVerb}
(step t10 (cl (not (> (f a) (f b))) (not (= (f a) (f b))))
- :rule la_generic :args (1.0 (- 1.0)))
+ :rule la_generic :args (1.0 -1.0))
\end{AletheVerb}
To verify this we have to check the insatisfiability of $(f\,a) > (f\,b) \land
@@ -495,7 +495,7 @@ not apply. Finally, after step~5 the conjunction is $(f\,a) - (f\,b) > 0 \land
The following \proofRule{la_generic} step is from a \textsf{QF\_UFLIA} problem:
\begin{AletheVerb}
(step t11 (cl (not (<= f3 0)) (<= (+ 1 (* 4 f3)) 1))
- :rule la_generic :args (1 (div 1 4)))
+ :rule la_generic :args (1.0 1/4))
\end{AletheVerb}
After normalization we get $-f_3 \geq 0 \land 4\times f_3 > 0$.
This time step~4 applies and we can strengthen this to