Commit d56b3247 authored by ehilin02's avatar ehilin02
Browse files

section 5.1

parent 62e8dadb
......@@ -80,7 +80,7 @@ In the sequel, we assume that $\abs(\varphi)$ is satisfiable and $\abs(\varphi)
Given the entailment problem $\varphi \models \psi$,
we denote by $\addr(\varphi)$ (and $\addr(\psi)$)
the set of terms used as start and end addresses of spatial atoms
the set of terms $\atomhead(a)$ and $\atomtail(a)$ for spatial atoms $a$
in $\varphi$ (resp. $\psi$).
%Moreover, let $\addr(\varphi,\psi)$ denote $\addr(\varphi) \cup \addr(\psi)$.
%
......@@ -132,7 +132,7 @@ C_\preceq \wedge \abs(\varphi) \mbox{ is satisfiable and }
C_\preceq \wedge \abs(\varphi) \models \abs(\psi).
\label{eq:order}
\end{align}
We consider that the atoms $\hls{}(t_1, t_2; t_3)$ in $\varphi$ or $\psi$ such that $C_\preceq \models t_1 = t_2$ are removed because they correspond to an empty heap.
We can remove the atoms $\hls{}(t_1, t_2; t_3)$ in $\varphi$ or $\psi$ such that $C_\preceq \models t_1 = t_2$ because they correspond to an empty heap.
Moreover, after a renaming,
we assume that the spatial atoms are sorted in each formula, namely,
the following two \PbA\ entailments hold:
......
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