From 2c379f562d16432383ff34ee308ba1b1b46b7116 Mon Sep 17 00:00:00 2001
From: Erin van der Veen
Date: Sun, 15 Apr 2018 20:26:27 +0200
Subject: Elimination Rules

---
 Assignment1/conversion.tex | 61 +++++++++++++++++++++++++++++++++++++---------
 1 file changed, 50 insertions(+), 11 deletions(-)

(limited to 'Assignment1')

diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 2ed3e47..24be26d 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -27,8 +27,8 @@ This rewrite system is given in Figure~\ref{fig:rewrite}.
 		&\Xop\phi       &&\leftrightarrow \bot \Uop \phi\\
 		&\Gop\phi       &&\leftrightarrow \neg (\top \Uop \neg \phi)\\
 		&\Fop\phi       &&\leftrightarrow \top \Uop \phi\\
-		&\Gop^{--1}\phi &&\leftrightarrow \neg (\top \Sop \neg \phi)\\
-		&\Fop^{--1}\phi &&\leftrightarrow \top \Sop \neg
+		&\Gop^{-1}\phi &&\leftrightarrow \neg (\top \Sop \neg \phi)\\
+		&\Fop^{-1}\phi &&\leftrightarrow \top \Sop \neg
 	\end{alignat*}
 	\caption{The rewrite rules for writing any PLTL formula as a formula containing only $\Sop$ and $\Uop$.}
 	\label{fig:rewrite}
@@ -42,21 +42,60 @@ Gabby proofs that this can by done in Theorem 2.4 of his paper,
 the rewrite rules are given in the Appendix of the same paper.
 In this book, we will not proof that these rewrite rules hold, but they are given below.
 First, however, note that there are 8 possible cases where there is a $\Uop$ in the scope of a $\Sop$.
-\begin{itemize}
+\begin{enumerate}
 	\item Suppose $E = q \Sop a \wedge (\alpha \Uop \beta))$ then it holds that $E = E_1 \vee E_2 \vee E_3$ if:
-	\begin{align*}
-		E_1 &= (q \Sop a) \wedge (\alpha \Sop a) \wedge \alpha (\alpha \Uop \beta)\\
-		E_2 &= \beta \wedge (\alpha \Sop a) \wedge (q \Sop a)\\
-		E_3 &= q \Sop \beta \wedge q \wedge (\alpha \Sop a) \wedge (q \Sop a)
-	\end{align*}
+		\begin{align*}
+			E_1 &= (q \Sop a) \wedge (\alpha \Sop a) \wedge \alpha (\alpha \Uop \beta)\\
+			E_2 &= \beta \wedge (\alpha \Sop a) \wedge (q \Sop a)\\
+			E_3 &= q \Sop \beta \wedge q \wedge (\alpha \Sop a) \wedge (q \Sop a)
+		\end{align*}
 
-	\item Suppose $E = q \Sop a \wedge \neg (a \Uop \beta)$ then it holds that $E = E_1 \vee E_2 \vee E_3$ if:
+	\item Suppose $E = q \Sop a \wedge \neg (\alpha \Uop \beta)$ then it holds that $E = E_1 \vee E_2 \vee E_3$ if:
 		\begin{align*}
 			E_1 &= (a \wedge \neg \beta \Sop a) \wedge \neg \beta \wedge \neg (\alpha \Uop \beta)\\
 			E_2 &= \neg \beta \wedge \neg \alpha \wedge (\neg \beta \wedge q \Sop a)\\
-		E_3 &= a\Sop\neg\beta \wedge \neg \alpha \wedge q \wedge (q \wedge \neg\beta \Sop a)
+			E_3 &= a\Sop\neg\beta \wedge \neg \alpha \wedge q \wedge (q \wedge \neg\beta \Sop a)
+		\end{align*}
+
+	\item Suppose $E = q \Sop a \wedge \neg (\alpha \Sop \beta)$ then it holds that $E = E_1 \vee E_2 \vee E_3$ if:
+		\begin{align*}
+			E_1 &= (q \wedge \neg \beta \Sop a) \wedge \neg \beta \wedge \neg (\alpha \Uop \beta)\\
+			E_2 &= \neg \beta \wedge \neg \alpha \wedge (\neg \beta \wedge q \Sop a)\\
+			E_3 &= q \Sop (\neg \beta \wedge \neg \alpha \wedge q \wedge (\neg \beta \wedge q \Sop a))
 		\end{align*}
-\end{itemize}
+
+	\item Suppose $E = q \vee \neg (\alpha \Uop \beta) \Sop a$ then it holds that $E = \neg (\neg a \Sop \neg q \wedge (\alpha \Uop \beta) \wedge \neg a) \wedge \Fop^{-1} a$,
+		which can be reduced via rule 1.
+
+	\item Suppose $E = q \vee (\alpha \Uop \beta) \Sop a \wedge (\alpha \Uop \beta)$ then it holds that $E = E_1 \vee (E_2 \wedge E_3)$ if:
+		\begin{align*}
+			E_1 &= (\alpha \Sop a) \wedge (\beta \vee (\alpha \wedge (\alpha \Uop \beta)))\\
+			E_2 &= (\beta \vee \alpha \vee \neg(\neg\beta \Sop \neg q) \Sop \beta \wedge (\alpha \Sop a))\\
+			E_3 &= (\beta \vee (\alpha \wedge (\alpha \Uop \beta))) \vee \neg (\neg\beta \Sop \neg q)
+		\end{align*}
+	
+	\item Suppose $E = q \vee (\alpha \Uop \beta) \Sop a \wedge \neg(\alpha \Uop \beta)$ then it holds that $E = E_1 \vee E_2 \vee E_3$ if:
+		\begin{align*}
+			E_1 &= (\neg \beta \wedge q \Sop a) \wedge \neg \beta \wedge \neg \alpha\\
+			E_2 &= q \vee (\alpha \Uop \beta) \Sop \neg \beta \wedge \neg \alpha \wedge (q \vee (\alpha \Uop \beta)) \wedge (\neg \beta \wedge q \Sop a)\\
+			E_3 &= (q \wedge \neg \beta \Sop a) \wedge \neg \beta \wedge \neg (\alpha \Uop \beta)
+		\end{align*}
+
+	\item Suppose $E = q \vee \neg(\alpha \Uop \beta) \Sop a \wedge (\alpha \Uop \beta)$ then it holds that $E = E_1 \vee E_2$ if:
+		\begin{align*}
+			E_1 &= (q \vee \neg (\alpha \Uop \beta) \Sop \beta \wedge (q \vee \neg (\alpha \Uop \beta)) \wedge (\alpha \wedge q \Sop a))\\
+			E_2 &= (\alpha \wedge q \Sop a) \wedge \alpha \wedge (\alpha \Uop \beta)
+		\end{align*}
+		Where $E_1$ can be further reduced using eliminations 8 and 4.
+	\item Suppose $E = q \vee \neg (\alpha \Uop \beta) \Sop a \wedge \neg (\alpha \Uop \beta)$ then it holds that $E = \neg \Gop^{-1}(E_1 \vee E_2 \vee E_3)$ if:
+		\begin{align*}
+			E_1 &= \neg a \vee \neg (\alpha \Uop \beta)\\
+			E_2 &= \neg a \vee (\alpha \Uop \beta) \Sop \neg q \wedge (\alpha \Uop \beta) \wedge \neg a\\
+			E_3 &= \neg a \vee (\alpha \Uop \beta) \Sop \neg q \wedge (\alpha \Uop \beta)
+		\end{align*}
+		After elimination of $\Gop^{-1}$, this formula can be further eliminated.
+		In particular by using elimination 5.
+\end{enumerate}
 
 \paragraph{Automata-based Algorithm}
 
-- 
cgit v1.2.3