From 9dab69e5001fba4403a1e1a2f1ad9599dd637d4b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Hans-J=C3=B6rg=20Schurr?= <hansjoerg-schurr@uiowa.edu>
Date: Fri, 20 Jan 2023 14:49:10 -0600
Subject: [PATCH] Remove trailing whitespaces
---
spec/changelog.tex | 2 +-
spec/doc.tex | 48 +++++++++++++++++++++++-----------------------
spec/rule_list.tex | 44 +++++++++++++++++++++---------------------
3 files changed, 47 insertions(+), 47 deletions(-)
diff --git a/spec/changelog.tex b/spec/changelog.tex
index 59f2eb5..ca49bf1 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -46,7 +46,7 @@ The language has a formal definition and a proof of soundness. The syntax
describes how proofs are encoded in the text file.
The syntax was extended to allow extra annotations. Tools consuming Alethe
-proofs must be able to ignore such extra annotations.
+proofs must be able to ignore such extra annotations.
List of rules:
\begin{itemize}
diff --git a/spec/doc.tex b/spec/doc.tex
index 738d5e5..553f4b1 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -176,7 +176,7 @@ break
\end{inner-rule}
}
-\theoremstyle{definition}
+\theoremstyle{definition}
\newtheorem{RuleExample}{Example}[inner-rule]
% TODO: synchronize colors!
@@ -403,10 +403,10 @@ The paragraphs below describe the concepts necessary to
understand the proof step by step.
\begin{Alethe}
-1.& \ctxsep & $\forall x.\, (P\,x)$ & $ \proofRule{assume}$ \\
-2.& \ctxsep & $\neg (P\,a) $ & $ \proofRule{assume}$ \\
-3.& \ctxsep & $\neg (\forall x.\, (P\,x)) \lor (P\,a)$ & $\proofRule{forall_inst}\,[(x, a)]$ \\
-4.& \ctxsep & $\neg (\forall x.\, (P\,x)), (P\,a)$ & $ (\proofRule{or}\:3)$ \\
+1.& \ctxsep & $\forall x.\, (P\,x)$ & $ \proofRule{assume}$ \\
+2.& \ctxsep & $\neg (P\,a) $ & $ \proofRule{assume}$ \\
+3.& \ctxsep & $\neg (\forall x.\, (P\,x)) \lor (P\,a)$ & $\proofRule{forall_inst}\,[(x, a)]$ \\
+4.& \ctxsep & $\neg (\forall x.\, (P\,x)), (P\,a)$ & $ (\proofRule{or}\:3)$ \\
5.& \ctxsep & $\bot $ & $ (\proofRule{resolution}\: 1, 2, 4)$ \\
\end{Alethe}
@@ -500,7 +500,7 @@ introduce local assumptions. The \proofRule{subproof} {\em rule} discharges the
local assumptions.
From an
assumption $\varphi$ and a formula $\psi$ proved
-from $\varphi$, the \proofRule{subproof} rule deduces the clause $\neg \varphi,
+from $\varphi$, the \proofRule{subproof} rule deduces the clause $\neg \varphi,
\psi$ that discharges the local assumption $\varphi$.
%
A \proofRule{subproof} step cannot use a premise from a subproof nested
@@ -518,15 +518,15 @@ formula $(2 + 2) ≈ 5$. The proof uses a subproof to prove the
lemma $((2 + 2) ≈ 5) \Rightarrow 4 ≈ 5$.
\begin{Alethe}
-1.& \ctxsep & $(2 + 2) ≈ 5$ & $\proofRule{assume}$ \\
-2.& \spctxsep & $(2 + 2) ≈ 5 $ & $\proofRule{assume}$ \\
-3.& \spctxsep & $(2 + 2) ≈ 4 $ & $\proofRule{sum_simplify}$ \\
+1.& \ctxsep & $(2 + 2) ≈ 5$ & $\proofRule{assume}$ \\
+2.& \spctxsep & $(2 + 2) ≈ 5 $ & $\proofRule{assume}$ \\
+3.& \spctxsep & $(2 + 2) ≈ 4 $ & $\proofRule{sum_simplify}$ \\
4.& \spctxsep & $4 ≈ 5 $ & $(\proofRule{trans}\ 2, 3)$ \\
\spsep
-5.& \ctxsep & $\neg((2 + 2) ≈ 5), 4 ≈ 5$ & $\proofRule{subproof}$ \\
-6.& \ctxsep & $(4 ≈ 5)≈ \bot$ & $\proofRule{eq_simplify}$ \\
-7.& \ctxsep & $\neg((4 ≈ 5)≈ \bot), \neg(4≈ 5), \bot $ & $\proofRule{equiv_pos2}$ \\
-8.& \ctxsep & $\bot $ & $(\proofRule{resolution}\ 1, 5, 6, 7)$ \\
+5.& \ctxsep & $\neg((2 + 2) ≈ 5), 4 ≈ 5$ & $\proofRule{subproof}$ \\
+6.& \ctxsep & $(4 ≈ 5)≈ \bot$ & $\proofRule{eq_simplify}$ \\
+7.& \ctxsep & $\neg((4 ≈ 5)≈ \bot), \neg(4≈ 5), \bot $ & $\proofRule{equiv_pos2}$ \\
+8.& \ctxsep & $\bot $ & $(\proofRule{resolution}\ 1, 5, 6, 7)$ \\
\end{Alethe}
\end{example}
@@ -543,7 +543,7 @@ denoted $x_i\mapsto t_i$.
In the first case, we say that $c_i$ {\em fixes} the
variable. The second case is a mapping.
Throughout this chapter, $\Gamma$ denotes
-an arbitrary context.
+an arbitrary context.
% TODO: define \subst and related
Every context $\Gamma$ induces a substitution
@@ -716,7 +716,7 @@ as if proxy names introduced by \inlineAlethe{:named} annotations have been
expanded and annotations have been removed. For example, the term
\inlineAlethe{(or (! (P a) :named baz) (! baz :foo))} and
\inlineAlethe{(or (P a) (P a))} are considered to be syntactically equal.
-Here \inlineAlethe{:foo} is an arbitrary {\smtlib} annotation.
+Here \inlineAlethe{:foo} is an arbitrary {\smtlib} annotation.
Figure~\ref{fig:grammar} shows the grammar of the proof text. It
is based on the {\smtlib} grammar, as defined in the {\smtlib}
@@ -976,10 +976,10 @@ $C_i$ in $P$ uses $i$ as its index.
The context
only changes at anchors and subproof-concluding steps.
Therefore, the elements of $C_1, \dots, C_n$ that are steps
-are not associated with a context.
+are not associated with a context.
Instead, the context can be computed
from the prior anchors.
-The anchors only ever extend the context.
+The anchors only ever extend the context.
To check an Alethe proof we can iteratively eliminate the first-innermost
subproof, i.e., the innermost subproof that does not come after a
@@ -1157,7 +1157,7 @@ It is useful to give precise semantics
to contexts to have the tools to check that rules that use contexts
are sound.
Contexts are local in the sense that they affect only the
-proof step they are applied to.
+proof step they are applied to.
For the full details on contexts see~\cite{barbosa-2019}.
The presentation here is adapted from this publication, but omits some
details.
@@ -1361,7 +1361,7 @@ nested subproofs.
$\psi_{\mathit{start}+n} \vDash \psi_{\mathit{start}+n}$ which can
be weakened to $V_n \vDash \psi_{\mathit{start}+n}$.
In the first case, the step $C_{\mathit{start}+n}$ has a set of
- premises $S$.
+ premises $S$.
For each step $C_{\mathit{start}+i} \in S$ we have $i < n$ and
$V_i \vDash \psi_{\mathit{start}+i}$ due to the induction
hypothesis. Since $i < n$, the premises $V_i$ are a subset of $V_n$ and
@@ -1385,7 +1385,7 @@ nested subproofs.
\vDash \neg\varphi_1, \cdots, \neg\varphi_m, l_1, \dots, l_o.
\]
where $l_1, \dots, l_o$ are the literals of $\psi_{\mathit{end}-1}$.
- This clause is exactly the conclusion of the
+ This clause is exactly the conclusion of the
step $C_{\mathit{end}}$
according to the definition of the \proofRule{subproof} rule.
\end{proof}
@@ -1411,7 +1411,7 @@ subproofs with contexts. This is slightly complicated by the
C_{\mathit{start}}]$ where $δ$ is either the largest index
$δ < {\mathit{start}}$ such
that $s_{δ}$ is an anchor, or $1$ if no such index exist.
- Hence, there is no anchor between $C_{δ}$ and $C_{\mathit{start}}$.
+ Hence, there is no anchor between $C_{δ}$ and $C_{\mathit{start}}$.
\end{lemma}
\begin{proof}
The step $C_{\mathit{start}}$ is an anchor due to the definition
@@ -1458,7 +1458,7 @@ $\mathit{end}$. & $\Gamma$ & \ctxsep & $\psi$ & $(\ruleType{rule}\
depend on some \proofRule{assume} steps that appear before them
in their subproof. This is the case if the steps are outermost steps, or
if the subproof that starts at $C_{δ}$ concludes with
- a \proofRule{subproof} step.
+ a \proofRule{subproof} step.
%
In this case we can, as we saw in the proof of
Lemma~\ref{lem:sound_subproof}, weaken their judgments to include
@@ -1626,7 +1626,7 @@ The left-hand side is a formula starting with an existential quantifier
over some variable $x$. In the formula on the right-hand side, the
variable is replaced by the appropriate Skolem term.
To provide a proof for the replacement, the \proofRule{sko_ex} step
-uses one premise.
+uses one premise.
The premise
has a context that maps the existentially quantified variable
to the appropriate Skolem term.
@@ -1649,7 +1649,7 @@ is functional congruence, and \proofRule{sko_forall} works like
\begin{AletheS}
1. & \spctx{$x\mapsto (\varepsilon x.\,\neg (p\,x))$}
& \ctxsep
- & $x ≈ \varepsilon x.\,\neg (p\,x) $ &
+ & $x ≈ \varepsilon x.\,\neg (p\,x) $ &
$\proofRule{refl}$ \\
2. & \spctx{$x\mapsto (\varepsilon x.\,\neg (p\,x))$} & \ctxsep & $ (p\,x) ≈ p(\varepsilon x.\,\neg (p\,x))$ & $(\proofRule{cong}\, 1)$ \\
\spsep
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 84c984e..479bd14 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -292,7 +292,7 @@ This rule is the resolution of two or more clauses.
$i_1$. & \ctxsep & $l^1_1$, $\dots$, $l^1_{k^1}$ & ($\ruleType{...}$) \\
\aletheLine
$i_n$. & \ctxsep & $l^n_1$, $\dots$, $l^n_{k^n}$ & ($\ruleType{...}$) \\
- $j$. & \ctxsep & $l^{r_1}_{s_1}$, $\dots$, $l^{r_m}_{s_m}$ & ($\currule\;i_1,\dots, i_n$) \\
+ $j$. & \ctxsep & $l^{r_1}_{s_1}$, $\dots$, $l^{r_m}_{s_m}$ & ($\currule\;i_1,\dots, i_n$) \\
\end{AletheX}
where $l^{r_1}_{s_1} , \dots , l^{r_m}_{s_m}$ are from $l^{i}_{j}$ and
are the result of a chain of predicate resolution steps on the clauses of
@@ -356,11 +356,11 @@ last step of the subproof is the conclusion.
\begin{AletheX}
$i_1$. & \spctxsep & $\varphi_1$ & $\proofRule{assume}$ \\
\aletheLine
-$i_n$. & \spctxsep & $\varphi_n$ & $\proofRule{assume}$ \\
+$i_n$. & \spctxsep & $\varphi_n$ & $\proofRule{assume}$ \\
\aletheLineB
$j$. & \spctxsep & $\psi$ & ($\dots$) \\
\spsep
-k. & \ctxsep & $\neg\varphi_1$,\dots, $\neg\varphi_n$, $\psi$ & $\proofRule{subproof}$ \\
+k. & \ctxsep & $\neg\varphi_1$,\dots, $\neg\varphi_n$, $\psi$ & $\proofRule{subproof}$ \\
\end{AletheX}
\end{RuleDescription}
@@ -402,10 +402,10 @@ each $i$, let $\varphi := \varphi_i$ and $a := a_i$.
\begin{enumerate}
\item If $\varphi = s_1 > s_2$, then let $\varphi := s_1 \leq s_2$.
If $\varphi = s_1 \geq s_2$, then let $\varphi := s_1 < s_2$.
- If $\varphi = s_1 < s_2$, then let $\varphi := s_1 \geq s_2$.
+ If $\varphi = s_1 < s_2$, then let $\varphi := s_1 \geq s_2$.
If $\varphi = s_1 \leq s_2$, then let $\varphi := s_1 > s_2$. This negates
the literal.
- \item If $\varphi = \neg (s_1 \bowtie s_2)$, then let $\varphi := s_1 \bowtie s_2$.
+ \item If $\varphi = \neg (s_1 \bowtie s_2)$, then let $\varphi := s_1 \bowtie s_2$.
\item Replace $\varphi$ by $\sum_{i=0}^{n}c_i\times{}t_i - \sum_{i=n+1}^{m} c_i\times{}t_i
\bowtie d$ where $d := d_2 - d_1$.
\item \label{la_generic:str}Now $\varphi$ has the form $s_1 \bowtie d$. If all
@@ -453,7 +453,7 @@ To verify this we have to check the insatisfiability of $(f\,a) > (f\,b) \land
(f\,a) - (f\,b) ≈ 0$. Since we don't have an integer sort in this logic step~4 does
not apply. Finally, after step~5 the conjunction is $(f\,a) - (f\,b) > 0 \land
- (f\,a) + (f\,b) ≈ 0$. This sums to $0 > 0$, which is a contradiction.
-\end{RuleExample}
+\end{RuleExample}
\begin{RuleExample}
The following \proofRule{la_generic} step is from a \textsf{QF\_UFLIA} problem:
@@ -487,7 +487,7 @@ can be NP-hard. Hence, this rule should be avoided when possible.
\begin{RuleDescription}{la_disequality}
\begin{AletheX}
-$i$. & \ctxsep &
+$i$. & \ctxsep &
$t_1 ≈ t_2 \lor \neg (t_1 \leq t_2) \lor \neg (t_2 \leq t_1)$
& (\currule) \\
\end{AletheX}
@@ -513,7 +513,7 @@ checking the \proofRule{la_generic} the result is trivially unsatisfiable.
The second form handles bounds on linear combinations. It is binary clause:
\begin{AletheX}
-$i$. & \ctxsep &
+$i$. & \ctxsep &
$\varphi_1 \lor \varphi_2$ % Checked: this is a proper disjunction not a cl
& (\currule) \\
\end{AletheX}
@@ -540,7 +540,7 @@ as for the rule \proofRule{la_generic}.
$j$. & \spctx{ $\Gamma, y_1,\dots, y_n, x_1 \mapsto y_1, \dots , x_n \mapsto y_n$}
& \ctxsep & $\varphi ≈ \varphi'$ & ($\dots$) \\
\spsep
-$k$. & & \ctxsep &
+$k$. & & \ctxsep &
$\forall x_1, \dots, x_n.\varphi ≈ \forall y_1, \dots, y_n. \varphi'$
& \currule{} \\
\end{AletheXS}
@@ -568,7 +568,7 @@ The \currule{} rule skolemizes universal quantifiers.
\begin{AletheXS}
\aletheLineS
-$j$. &
+$j$. &
\spctx{$\Gamma, x_1 \mapsto (\varepsilon x_1.\neg\varphi), \dots, x_n \mapsto (\varepsilon x_n.\neg\varphi)$}
& \ctxsep & $\varphi ≈ \psi$ & ($\dots$) \\
\spsep
@@ -579,7 +579,7 @@ $k$. & & \ctxsep & $\forall x_1, \dots, x_n.\varphi ≈ \psi$ & \currule{} \\
\begin{RuleDescription}{forall_inst}
\begin{AletheX}
-$i$. & \ctxsep &
+$i$. & \ctxsep &
$\neg (\forall x_1, \dots, x_n. P) \lor P[x_1\mapsto t_1]\dots[x_n\mapsto t_n]$
& \currule\, [$(x_{k_1}, t_{k_1})$, $\dots$, $(x_{k_n}, t_{k_n})$] \\
\end{AletheX}
@@ -637,7 +637,7 @@ $t_1 ≈ t_n$ & \currule \\
\begin{RuleDescription}{eq_congruent}
\begin{AletheX}
-$i$. & \ctxsep &
+$i$. & \ctxsep &
$\neg (t_1 ≈ u_1)$, $\dots$ ,$\neg (t_n ≈ u_n)$,
$(f\,t_1\, \cdots\,t_n) ≈ (f\,u_1\, \cdots\,u_n)$
& \currule \\
@@ -647,7 +647,7 @@ $(f\,t_1\, \cdots\,t_n) ≈ (f\,u_1\, \cdots\,u_n)$
\begin{RuleDescription}{eq_congruent_pred}
\begin{AletheX}
-$i$. & \ctxsep &
+$i$. & \ctxsep &
$\neg (t_1 ≈ u_1)$, \dots ,$\neg (t_n ≈ u_n)$,
$(P\,t_1\, \cdots\,t_n) ≈ (P\,u_1\, \cdots\,u_n)$
& \currule \\
@@ -657,7 +657,7 @@ where $P$\, is a function symbol with co-domain sort $\lsymb{Bool}$.
\begin{RuleDescription}{qnt_cnf}
\begin{AletheX}
-$i$. & \ctxsep &
+$i$. & \ctxsep &
$\neg(\forall x_1, \dots, x_n. \varphi) \lor \forall x_{k_1}, \dots, x_{k_m}.\varphi'$
& \currule \\
\end{AletheX}
@@ -715,7 +715,7 @@ and $1 \leq k \leq n$.
\begin{RuleDescription}{or}
\begin{AletheX}
-$i$. & \ctxsep &
+$i$. & \ctxsep &
$\varphi_1 \lor \cdots \lor \varphi_n$ & ($\dots$) \\
$j$. & \ctxsep & $\varphi_1, \dots, \varphi_n$ & (\currule\;$i$) \\
\end{AletheX}
@@ -967,25 +967,25 @@ $j$. & \ctxsep & $\neg\varphi_1 , \neg\varphi_2$ & (\currule\;$i$) \\
This rule is used to replace connectives by their definition. It can be one
of the following:
\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ &
+$i$. & \ctxsep & $\Gamma$ &
$(\lsymb{xor}\,\varphi_1\,\varphi_2) ≈
((\neg\varphi_1 \land \varphi_2) \lor (\varphi_1 \land \neg\varphi_2))$ & \currule \\
\end{AletheXS}
\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ &
+$i$. & \ctxsep & $\Gamma$ &
$(\varphi_1 ≈ \varphi_2) ≈
((\varphi_1 \rightarrow \varphi_2) \land (\varphi_2 \rightarrow \varphi_1))$ & \currule \\
\end{AletheXS}
\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ &
+$i$. & \ctxsep & $\Gamma$ &
$(\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3) ≈
((\varphi_1 \rightarrow \varphi_2) \land (\neg\varphi_1 \rightarrow \varphi_3))$ & \currule \\
\end{AletheXS}
\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ &
+$i$. & \ctxsep & $\Gamma$ &
$(\forall x_1, \dots, x_n.\,\varphi) ≈ \neg(\exists x_1, \dots, x_n.\,
\neg\varphi)$ & \currule \\
\end{AletheXS}
@@ -1407,7 +1407,7 @@ $i_n$. & $\Gamma$ & \ctxsep & $t_{n} ≈ s_{n}$ & ($\dots$) \\
$j$. & \spctx{$\Gamma, x_1 \mapsto s_1, \dots, x_n \mapsto s_n$}
& \ctxsep & $u ≈ u'$ & ($\dots$) \\
\spsep
-$k$. & $\Gamma$ & \ctxsep &
+$k$. & $\Gamma$ & \ctxsep &
$(\lsymb{let}\,x_1 = t_1,\, \dots,\, x_n = t_n\,\lsymb{in}\, u) ≈ u'$
& (\currule{}\;$i_1$, \dots, $i_n$) \\
\end{AletheXS}
@@ -1430,7 +1430,7 @@ If applied to terms of type $\lsymb{Bool}$ more than two terms can never be
distinct, hence only two cases are possible:
\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ &
+$i$. & \ctxsep & $\Gamma$ &
$(\lsymb{distinct}\,\varphi\,\psi) ≈ \neg (\varphi ≈ \psi)$ & \currule \\
\end{AletheXS}
and
@@ -1443,7 +1443,7 @@ $(\lsymb{distinct}\,\varphi_1\,\varphi_2\,\varphi_3\,\dots) ≈ \bot$ & \currule
The general case is
\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ &
+$i$. & \ctxsep & $\Gamma$ &
$(\lsymb{distinct}\,t_1\,\dots\, t_n) ≈
\bigwedge_{i=1}^{n}\bigwedge_{j=i+1}^{n} t_i\;{\not≈}\;t_j$ & \currule \\
\end{AletheXS}
--
GitLab