Skip to content
Snippets Groups Projects
Commit 17dd1226 authored by Hans-Jörg's avatar Hans-Jörg
Browse files

Remove redundant simplification from `implies_simplify`

The simplification `(P -> Q) -> Q => P or Q` is already covered
by `bool_simplify`.
parent b4032d3f
No related branches found
No related tags found
No related merge requests found
Pipeline #10977 passed
......@@ -26,6 +26,13 @@ following changes were implemented in this release.
\item An index that lists all proof rules was added.
\end{itemize}
Proof rules:
\begin{itemize}
\item The rule \proofRule{implies_simplify} is no longer allowed to
perform the simplification $(\varphi_1\rightarrow \varphi_2)\rightarrow \varphi_2
\varphi_1\lor \varphi_2$. This is covered by \proofRule{bool_simplify}.
\end{itemize}
\subsection*{0.2 --- \DTMdisplaydate{2022}{12}{19}{-1}}
This is an intermediate release. It collects all changes to the original
......
......@@ -1084,7 +1084,6 @@ The possible transformations are:
\item $ \varphi \rightarrow \varphi\top$
\item $\neg \varphi \rightarrow \varphi\varphi$
\item $ \varphi \rightarrow \neg \varphi\neg \varphi$
\item $( \varphi_1\rightarrow \varphi_2)\rightarrow \varphi_2\varphi_1\lor \varphi_2$
\end{itemize}
\end{RuleDescription}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment