Commit d9cf24ad authored by Mihaela SIGHIREANU's avatar Mihaela SIGHIREANU
Browse files

coNP fixes

parent 209dfbb6
......@@ -19,7 +19,6 @@ for any stack $s$, $s\models \chi$
We suppose that both formula $\varphi$ and $\psi$ have been transformed in normal form as follows:
\begin{itemize}
\item atoms $\hls{}(x,y;v')$ with $\abs(\varphi)\models (v'<2 \lor x=y)$ have been removed and replaced by $x=y$\mihaela{use $\xi$ ?}
\item atoms $\hls{}(x,y;v')$ with $\abs(\varphi)\models v'=2$ have been replaced by $y-x=2 : x\pto 2 \star \blk(x+1,y)$
\item ...\mihaela{TODO}
\end{itemize}
The normalization can be done in a linear number of calls to the \EPbA\ procedure.
......@@ -28,7 +27,7 @@ The formula $\chi$ shall ensure that $\varphi$ is satisfiable, so
it contains as conjunct $\abs(\varphi)$.
The entailment may be invalid iff one of the following holds:
\begin{itemize}
\begin{enumerate}
\item $\psi$ is not satisfiable, i.e., $\abs(\psi)$ is not satisfiable.
\item there exists an address inside a spatial atom of $\varphi$
......@@ -62,6 +61,6 @@ The entailment may be invalid iff one of the following holds:
that can not be filded into a $\hls{}$ atom with chunks of maximal size less or equal to $v'$\mihaela{difficult in P!}
\end{itemize}
\end{enumerate}
\end{proof}
Markdown is supported
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