From 1a0dcf4f69af477d8eb0bd4d6b49e4c3845aa610 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 17 Oct 2017 17:58:59 +0200 Subject: [PATCH] document the recent changes to implication rules * doc/tl/tl.tex: This adds the rules implemented in 0a2bca137 for #293. --- doc/tl/tl.tex | 122 ++++++++++++++++++++++++++++---------------------- 1 file changed, 69 insertions(+), 53 deletions(-) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index dbaad34ce..1670668dd 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -118,6 +118,7 @@ \newcommand{\equivM}{\stackrel{\dag}{\equiv}} \def\limplies{\rightarrow} +\def\simpe{\rightleftharpoons} \def\simp{\rightrightharpoons} \def\Simp{\stackrel{+}{\simp}} \def\liff{\leftrightarrow} @@ -1724,60 +1725,75 @@ In the following rewritings rules, $f\simp g$ means that $g$ was proved to be implied by $f$ using either of the above two methods. Additionally, implications denoted by $f\Simp g$ are only checked if the ``\verb|tl_simplifier_options::containment_checks_stronger|'' -option is set (otherwise the rewriting rule is not applied). As in -the previous section, formulas $e$ and $u$ represent respectively -pure eventualities and purely universal formulas. +option is set (otherwise the rewriting rule is not applied). We write +$f\simpe g$ iff $f\simp g$ and $f\simp f$. -\begin{equation*} -\begin{array}{cccr@{\,}l} -\text{if}& f\simp g &\text{then}& f\OR g &\equiv g \\ -\text{if}& f\simp g &\text{then}& f\AND g &\equiv f \\ -\text{if}& f\simp \NOT g &\text{then}& f\OR g &\equiv \1 \\ -\text{if}& f\simp \NOT g &\text{then}& f\AND g &\equiv \0 \\ -\text{if}& f\simp g &\text{then}& f\U g &\equiv g \\ -\text{if}& (f\U g)\Simp g &\text{then}& f\U g &\equiv g \\ -\text{if}& (\NOT f)\simp g &\text{then}& f\U g &\equiv \F g \\ -\text{if}& g\simp e &\text{then}& e\U g &\equiv \F g \\ -\text{if}& f\simp g &\text{then}& f\U (g \U h) &\equiv g \U h \\ -\text{if}& f\simp g &\text{then}& f\U (g \W h) &\equiv g \W h \\ -\text{if}& g\simp f &\text{then}& f\U (g \U h) &\equiv f \U h \\ -\text{if}& f\simp h &\text{then}& f\U (g \R (h \U k)) &\equiv g \R (h \U k) \\ -\text{if}& f\simp h &\text{then}& f\U (g \R (h \W k)) &\equiv g \R (h \W k) \\ -\text{if}& f\simp h &\text{then}& f\U (g \M (h \U k)) &\equiv g \M (h \U k) \\ -\text{if}& f\simp h &\text{then}& f\U (g \M (h \W k)) &\equiv g \M (h \W k) \\ -\text{if}& f\simp h &\text{then}& (f\U g) \U h &\equiv g \U h \\ -\text{if}& f\simp h &\text{then}& (f\W g) \U h &\equiv g \U h \\ -\text{if}& g\simp h &\text{then}& (f\U g) \U h &\equiv (f \U g) \OR h \\ -\text{if}& f\simp g &\text{then}& f\W g &\equiv g \\ -\text{if}& (f\W g)\Simp g &\text{then}& f\W g &\equiv g \\ -\text{if}& (\NOT f)\simp g &\text{then}& f\W g &\equiv \1 \\ -\text{if}& f\simp g &\text{then}& f\W (g \W h) &\equiv g \W h \\ -\text{if}& g\simp f &\text{then}& f\W (g \U h) &\equiv f \W h \\ -\text{if}& g\simp f &\text{then}& f\W (g \W h) &\equiv f \W h \\ -\text{if}& f\simp h &\text{then}& (f\U g) \W h &\equiv g \W h \\ -\text{if}& f\simp h &\text{then}& (f\W g) \W h &\equiv g \W h \\ -\text{if}& g\simp h &\text{then}& (f\W g) \W h &\equiv (f \W g) \OR h \\ -\text{if}& g\simp h &\text{then}& (f\U g) \W h &\equiv (f \U g) \OR h \\ -\text{if}& g\simp f &\text{then}& f\R g &\equiv g \\ -\text{if}& g\simp \NOT f &\text{then}& f\R g &\equiv \G g \\ -\text{if}& u\simp g &\text{then}& u\R g &\equiv \G g \\ -\text{if}& g\simp f &\text{then}& f\R (g \R h) &\equiv g \R h \\ -\text{if}& g\simp f &\text{then}& f\R (g \M h) &\equiv g \M h \\ -\text{if}& f\simp g &\text{then}& f\R (g \R h) &\equiv f \R h \\ -\text{if}& h\simp f &\text{then}& (f\R g) \R h &\equiv g \R h \\ -\text{if}& h\simp f &\text{then}& (f\M g) \R h &\equiv g \R h \\ -\text{if}& g\simp h &\text{then}& (f\R g) \R h &\equiv (f \AND g) \R h \\ -\text{if}& g\simp h &\text{then}& (f\M g) \R h &\equiv (f \AND g) \R h \\ -\text{if}& g\simp f &\text{then}& f\M g &\equiv g \\ -\text{if}& g\simp \NOT f &\text{then}& f\M g &\equiv \0 \\ -\text{if}& g\simp f &\text{then}& f\M (g \M h) &\equiv g \M h \\ -\text{if}& f\simp g &\text{then}& f\M (g \M h) &\equiv f \M h \\ -\text{if}& f\simp g &\text{then}& f\M (g \R h) &\equiv f \M h \\ -\text{if}& h\simp f &\text{then}& (f\M g) \M h &\equiv g \M h \\ -\text{if}& h\simp f &\text{then}& (f\R g) \M h &\equiv g \M h \\ -\text{if}& g\simp h &\text{then}& (f\M g) \M h &\equiv (f \AND g) \M h \\ -\end{array} -\end{equation*} +As in the previous section, formulas $e$ and $u$ represent +respectively pure eventualities and purely universal formulas. + +Finally $|f|_b$ denote the length of $f$ were all Boolean subformulas +are counted as one. + +\def\flessg{(f\simpe g) \land (|f|_b<|g|_b)} +\def\glessf{(f\simpe g) \land (|g|_b<|f|_b)} + +\begingroup +\allowdisplaybreaks +\begin{alignat*}{3} +\text{if~} & f\simp \NOT g && \text{~then~} & f\OR g & \equiv \1 \\ +\text{if~} & f\simp \NOT g && \text{~then~} & f\AND g & \equiv \0 \\ +\text{if~} & \flessg && \text{~then~} & f\OR g & \equiv f \\ +\text{if~} & f\simp g && \text{~then~} & f\OR g & \equiv g \\ +\text{if~} & \glessf && \text{~then~} & f\AND g & \equiv g \\ +\text{if~} & f\simp g && \text{~then~} & f\AND g & \equiv f \\ +\text{if~} & \flessg && \text{~then~} & f\U g & \equiv f \\ +\text{if~} & f\simp g && \text{~then~} & f\U g & \equiv g \\ +\text{if~} & (f\U g)\Simp g && \text{~then~} & f\U g & \equiv g \\ +\text{if~} & (\NOT f)\simp g && \text{~then~} & f\U g & \equiv \F g \\ +\text{if~} & g\simp e && \text{~then~} & e\U g & \equiv \F g \\ +\text{if~} & f\simp g && \text{~then~} & f\U (g \U h) & \equiv g \U h \\ +\text{if~} & f\simp g && \text{~then~} & f\U (g \W h) & \equiv g \W h \\ +\text{if~} & g\simp f && \text{~then~} & f\U (g \U h) & \equiv f \U h \\ +\text{if~} & f\simp h && \text{~then~} & f\U (g \R (h \U k)) & \equiv g \R (h \U k) \\ +\text{if~} & f\simp h && \text{~then~} & f\U (g \R (h \W k)) & \equiv g \R (h \W k) \\ +\text{if~} & f\simp h && \text{~then~} & f\U (g \M (h \U k)) & \equiv g \M (h \U k) \\ +\text{if~} & f\simp h && \text{~then~} & f\U (g \M (h \W k)) & \equiv g \M (h \W k) \\ +\text{if~} & f\simp h && \text{~then~} & (f\U g) \U h & \equiv g \U h \\ +\text{if~} & f\simp h && \text{~then~} & (f\W g) \U h & \equiv g \U h \\ +\text{if~} & g\simp h && \text{~then~} & (f\U g) \U h & \equiv (f \U g) \OR h \\ +\text{if~} & (\NOT f)\simp g && \text{~then~} & f\W g & \equiv \1 \\ +\text{if~} & \flessg && \text{~then~} & f\W g & \equiv f \\ +\text{if~} & f\simp g && \text{~then~} & f\W g & \equiv g \\ +\text{if~} & (f\W g)\Simp g && \text{~then~} & f\W g & \equiv g \\ +\text{if~} & f\simp g && \text{~then~} & f\W (g \W h) & \equiv g \W h \\ +\text{if~} & g\simp f && \text{~then~} & f\W (g \U h) & \equiv f \W h \\ +\text{if~} & g\simp f && \text{~then~} & f\W (g \W h) & \equiv f \W h \\ +\text{if~} & f\simp h && \text{~then~} & (f\U g) \W h & \equiv g \W h \\ +\text{if~} & f\simp h && \text{~then~} & (f\W g) \W h & \equiv g \W h \\ +\text{if~} & g\simp h && \text{~then~} & (f\W g) \W h & \equiv (f \W g) \OR h \\ +\text{if~} & g\simp h && \text{~then~} & (f\U g) \W h & \equiv (f \U g) \OR h \\ +\text{if~} & \flessg && \text{~then~} & f\R g & \equiv f \\ +\text{if~} & g\simp f && \text{~then~} & f\R g & \equiv g \\ +\text{if~} & g\simp \NOT f && \text{~then~} & f\R g & \equiv \G g \\ +\text{if~} & u\simp g && \text{~then~} & u\R g & \equiv \G g \\ +\text{if~} & g\simp f && \text{~then~} & f\R (g \R h) & \equiv g \R h \\ +\text{if~} & g\simp f && \text{~then~} & f\R (g \M h) & \equiv g \M h \\ +\text{if~} & f\simp g && \text{~then~} & f\R (g \R h) & \equiv f \R h \\ +\text{if~} & h\simp f && \text{~then~} & (f\R g) \R h & \equiv g \R h \\ +\text{if~} & h\simp f && \text{~then~} & (f\M g) \R h & \equiv g \R h \\ +\text{if~} & g\simp h && \text{~then~} & (f\R g) \R h & \equiv (f \AND g) \R h \\ +\text{if~} & g\simp h && \text{~then~} & (f\M g) \R h & \equiv (f \AND g) \R h \\ +\text{if~} & \flessg && \text{~then~} & f\M g & \equiv f \\ +\text{if~} & g\simp f && \text{~then~} & f\M g & \equiv g \\ +\text{if~} & g\simp \NOT f && \text{~then~} & f\M g & \equiv \0 \\ +\text{if~} & g\simp f && \text{~then~} & f\M (g \M h) & \equiv g \M h \\ +\text{if~} & f\simp g && \text{~then~} & f\M (g \M h) & \equiv f \M h \\ +\text{if~} & f\simp g && \text{~then~} & f\M (g \R h) & \equiv f \M h \\ +\text{if~} & h\simp f && \text{~then~} & (f\M g) \M h & \equiv g \M h \\ +\text{if~} & h\simp f && \text{~then~} & (f\R g) \M h & \equiv g \M h \\ +\text{if~} & g\simp h && \text{~then~} & (f\M g) \M h & \equiv (f \AND g) \M h \\ +\end{alignat*} +\endgroup Many of the above rules were collected from the literature~\cite{somenzi.00.cav,tauriainen.03.a83,babiak.12.tacas} and