From b95aa62b91aebdf8a36b567330a309a709d5be45 Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Fri, 16 Jul 2021 16:44:20 +0200
Subject: [PATCH] Improve some thing related to linear arithmetic
---
spec/changelog.tex | 5 +++--
spec/doc.tex | 30 +++++++++++++++---------------
spec/rule_list.tex | 3 ++-
3 files changed, 20 insertions(+), 18 deletions(-)
diff --git a/spec/changelog.tex b/spec/changelog.tex
index 95a38bc..69bbc74 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -9,8 +9,9 @@ List of rules:
Clarifications:
\begin{itemize}
\item Clarify functionality of choice in introduction.
- \item Add illustratory example to introduction.
- \item Normalize printing of (variable, term) arguments in the abstract notaton.
+ \item Add illustrating example to introduction.
+ \item Normalize printing of (variable, term) arguments in the abstract notation.
+ \item Fix linear arithmetic example in introduction.
\end{itemize}
\subsection*{0.1 --- \DTMdisplaydate{2021}{07}{10}{-1}}
diff --git a/spec/doc.tex b/spec/doc.tex
index 637f851..bc950bf 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -577,8 +577,6 @@ syntax for clauses uses the \smtinline{cl} operator, while disjunctions
use the standard SMT-LIB \smtinline{or} operator. The \proofRule{or}
\emph{rule} is responsible for converting disjunctions into clauses.
-% PF TODO: I would fix that just now, using an attribute to distinguish, and a
-% unique rule
The Alethe proofs use a generalized propositional
resolution rule with the rule name \proofRule{resolution} or
\proofRule{th\_resolution}. Both names denote the same rule. The
@@ -589,6 +587,13 @@ propositional; there is no notion of a unifier.
The premises of a resolution step are clauses and the conclusion
is a clause that has been derived from the premises by some binary
resolution steps.
+\begin{comment}{Hans-Jörg Schurr}
+We have to clarify that resolution counts the number of leading negations
+to determine polarity. This is important for double negation elimination.
+
+Furthermore, as Pascal noted, we should also fold the two rules into one
+and use an attribute to distinguish the two cases.
+\end{comment}
\paragraph{Quantifier Instantiation.}
To express quantifier instantiation, the rule \proofRule{forall\_inst}
@@ -623,20 +628,16 @@ of $(x+y<1) \lor (3<x)$, $x\simeq 2$, and $0\simeq y$.
\proofsep& 1.& (3 < x) \lor (x + y < 1) &(\proofRule{assume})\\
\proofsep& 2.& x\simeq 2 &(\proofRule{assume})\\
\proofsep& 3.& 0\simeq y &(\proofRule{assume})\\
-\proofsep& 4.& \neg (3<x) \lor \neg (x\simeq 2) &(\proofRule{la\_generic};\: ;1.0, 1.0)\\
-\proofsep& 5.& \neg (3<x) &(\proofRule{resolution}; 2, 4)\\
-\proofsep& 6.& x + y < 1 &(\proofRule{resolution}; 1, 5)\\
-\proofsep& 7.& \neg (x + y < 1) \lor \neg (x\simeq 2) \lor \neg (0 \simeq y)
-&(\proofRule{la\_generic};\: ;1.0, 1.0, 1.0)\\
-\proofsep& 8.& \bot &(\proofRule{resolution};\:\; 7, 6, 2, 3)
+\proofsep& 4.& (3 < x), (x + y < 1) &(\proofRule{or};1)\\
+\proofsep& 5.& \neg (3<x), \neg (x\simeq 2) &(\proofRule{la\_generic};\: ;1.0, 1.0)\\
+\proofsep& 6.& \neg (3<x) &(\proofRule{resolution}; 2, 5)\\
+\proofsep& 7.& x + y < 1 &(\proofRule{resolution}; 4, 6)\\
+\proofsep& 8.& \neg (x + y < 1), \neg (x\simeq 2) \lor \neg (0 \simeq y)
+&(\proofRule{la\_generic};\: ;1.0, -1.0, 1.0)\\
+\proofsep& 9.& \bot &(\proofRule{resolution};\:\; 8, 7, 2, 3)
\end{plListEq}
\end{example}
-% PF TODO 1 or -1 depends on the orientation of the equality...
-% x < 0 , x = 1 --> 1 1 gives 2x < 1
-% x < 0 , 1 = x --> 1 1 gives 1 < 0
-% this should somehow be fixed
-
\paragraph{Subproofs and Lemmas.}
The proof format uses subproof to prove lemmas and to manipulate the context.
To prove lemmas, a subproof can
@@ -645,8 +646,7 @@ local assumptions by concluding with an implication (written as a clause)
which has the local assumptions as its antecedents.
A step can only use steps from the same subproof as its premise. It
is not possible to have premises from either a subproof at a deeper
-level or from an outer level.%\todo{We could technically allow premises from
-%outside. Do we allow this?}
+level or from an outer level.
As the example below shows, our notation for subproofs is a
frame around the rules within the subproof. Subproofs are also used to
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index e0349c1..18c00ad 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -163,7 +163,8 @@ each $i$, let $\varphi := \varphi_i$ and $a := a_i$.
\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 \leq s_2$, then let $\varphi := s_1 > 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 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$.
--
GitLab