From caedbdc472f7dd14a07d1a988bb58b854db91ca5 Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Sun, 19 Jun 2022 21:50:49 +0200
Subject: [PATCH] Remove overloading of \bar{}
It was used in a few places to represent complementary literals,
but is mostly used to represent vectors of terms, variables. This
commit removes the usage for complementary literals. The few
places that used it now define the complement manually.
---
spec/doc.tex | 19 ++-----------------
spec/rule_list.tex | 25 ++++++++++++++++++++-----
2 files changed, 22 insertions(+), 22 deletions(-)
diff --git a/spec/doc.tex b/spec/doc.tex
index 648d9b7..5c93ec4 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -442,24 +442,9 @@ terms of sort $\mathbf{Bool}$.
%
We use $=$ to denote syntactic equality and $\simeq$ to denote the sorted
equality predicate.
-%
-We also use the notion of complementary literals
-very liberally: $\varphi = \bar{\psi}$ holds if the terms obtained
-after removing all leading negations from $\varphi$ and $\bar{\psi}$
-are syntactically equal and the number of leading negations is even
-for $\varphi$ and odd for $\psi$, or vice versa. To simplify the
+To simplify the
notation we will omit the sort of terms when possible.
-\begin{comment}{Haniel Barbosa}
- This notation is clashing with the notation of sequences of symbols, like in
- $\bar x$ for $x_1, \dots, x_n$.
-
- Maybe we could use an alternative notation for ``normalization under double
- negation elimination''? Like $\llfloor \varphi \rrfloor_{\neg\neg}$? I find
- the use of ``complementary literal'' to refer this a bit confusing
- anyway. There are very few uses in the rules (only tautology, and/or simps),
- so we could even not introduce a notation and just refer to ``normalized under
- double negation elimination''.
-\end{comment}
+
\begin{example} The following example shows a simple Alethe proof.
It uses quantifier instantiation and resolution to show a contradiction.
The sections below step-by-step describe the concepts necessary to
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 5f0decf..ed23cb8 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -87,7 +87,12 @@ serves only informational purpose.
\proofsep& j.& \top &(\currule; i)\\
\end{plList}
\end{plContainer}
- and $\varphi_i = \bar\varphi_j$.
+ and $\varphi_i$, $\varphi_j$ are such that
+ \begin{align*}
+ \varphi_i &= \underbrace{\neg \dots \neg}_n \psi \\
+ \varphi_j &= \underbrace{\neg \dots \neg}_m \psi
+ \end{align*}
+ and one of $n, m$ is odd and the other even. Either can be $0$.
\end{proof-rule}
\begin{proof-rule}{contraction}{veriT}
@@ -986,8 +991,13 @@ The possible transformations are:
\land \dots \land \varphi_{n'} $ where the right hand side has all
repeated literals removed.
\item $\varphi_1 \land\dots\land \bot\land\dots \land \varphi_n \leftrightarrow \bot$
- \item $\varphi_1 \land\dots\land \varphi_i\land \dots \land \varphi_j\land\dots \land \varphi_n \leftrightarrow \bot$ if
- $\varphi_i = \bar{\varphi_j}$
+ \item $\varphi_1 \land\dots\land \varphi_i\land \dots \land \varphi_j\land\dots \land \varphi_n \leftrightarrow \bot$
+ and $\varphi_i$, $\varphi_j$ are such that
+ \begin{align*}
+ \varphi_i &= \underbrace{\neg \dots \neg}_n \psi \\
+ \varphi_j &= \underbrace{\neg \dots \neg}_m \psi
+ \end{align*}
+ and one of $n, m$ is odd and the other even. Either can be $0$.
\end{itemize}
\end{proof-rule}
@@ -1014,8 +1024,13 @@ The possible transformations are:
\lor \dots \lor \varphi_{n'} $ where the right hand side has all
repeated literals removed.
\item $\varphi_1 \lor\dots\lor \top\lor\dots \lor \varphi_n \leftrightarrow \top$
- \item $\varphi_1 \lor\dots\lor \varphi_i\lor \dots \lor \varphi_j\lor\dots \lor \varphi_n \leftrightarrow \top$ if
- $\varphi_i = \bar{\varphi_j}$
+ \item $\varphi_1 \lor\dots\lor \varphi_i\lor \dots \lor \varphi_j\lor\dots \lor \varphi_n \leftrightarrow \top$
+ and $\varphi_i$, $\varphi_j$ are such that
+ \begin{align*}
+ \varphi_i &= \underbrace{\neg \dots \neg}_n \psi \\
+ \varphi_j &= \underbrace{\neg \dots \neg}_m \psi
+ \end{align*}
+ and one of $n, m$ is odd and the other even. Either can be $0$.
\end{itemize}
\end{proof-rule}
--
GitLab