Elimination Rules

1 files changed, 50 insertions, 11 deletions

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}