Commit 1a0dcf4f authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

document the recent changes to implication rules

* doc/tl/tl.tex: This adds the rules implemented in 0a2bca13
for #293.
parent 427c6969
......@@ -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.
\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*}
option is set (otherwise the rewriting rule is not applied). We write
$f\simpe g$ iff $f\simp g$ and $f\simp f$.
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
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment