From 5d615575aa80fe342eea133559755ddae8592a6f Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Thu, 15 Aug 2024 16:01:13 -0500
Subject: [PATCH] Add reordering rule
This addresses
https://gitlab.uliege.be/verit/alethe/-/issues/44
---
spec/changelog.tex | 2 ++
spec/rule_list.tex | 11 +++++++++++
2 files changed, 13 insertions(+)
diff --git a/spec/changelog.tex b/spec/changelog.tex
index d5b9489..555bca4 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -13,6 +13,8 @@ Proof rules:
and tedious use of \proofRule{subproof} for each direction of the equivalence.
\item Addition of the rule \proofRule{weakening} to express weakening of a
clause.
+ \item Addition of the \proofRule{reordering} rule to represent reordering of
+ the literals in a clause.
\end{itemize}
\noindent
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 26b3b84..02a5138 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -256,6 +256,7 @@ simplifications.}
\ruleref{la_mult_neg} & Multiplication with a negative factor.\\
\ruleref{symm} & Symmetry of equality. \\
\ruleref{not_symm} & Symmetry of not-equal.\\
+\ruleref{reordering} & Reording of the literals in a clause.\\
\end{xltabular}
\begin{xltabular}{\linewidth}{l X}
@@ -854,6 +855,16 @@ $j$. & \ctxsep & $\varphi_1, \cdots, \varphi_n, \psi_1, \dots, \psi_m$ & (\curru
where $m \geq 1$.
\end{RuleDescription}
+\begin{RuleDescription}{reordering}
+\begin{AletheX}
+$i$. & \ctxsep & $\varphi_1, \cdots, \varphi_n$ & ($\dots$) \\
+$j$. & \ctxsep & $\psi_1, \cdots, \psi_n$ & (\currule\;$i$) \\
+\end{AletheX}
+where the multisets $\{\varphi_1, \cdots, \varphi_n\}$ and $\{\psi_1, \cdots, \psi_n\}$
+are the same. That is, the conclusion of the rule is a reordering of the
+literals in the premise.
+\end{RuleDescription}
+
\begin{RuleDescription}{not_and}
\begin{AletheX}
$i$. & \ctxsep & $\neg (\varphi_1 \land \dots \land \varphi_n)$ & ($\dots$) \\
--
GitLab